Refiner.Univval formation : Tactic.Tp.tacval univ : Tactic.Chk.tacval nat : Tactic.Chk.tacval circle : Tactic.Chk.tacval pi : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tacval sg : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tacval signature : Tactic.KanTele.tac -> Tactic.Chk.tacval patch :
Tactic.Chk.tac ->
(Ident.t -> [ `Patch of Tactic.Chk.tac | `Subst of Tactic.Chk.tac ] option) ->
Tactic.Chk.tacval total : D.kan_tele -> D.con -> Tactic.Chk.tacval ext :
int ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tacval infer_nullary_ext : Tactic.Chk.tacval code_v :
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tacval coe :
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Syn.tacval hcom :
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Syn.tacval hcom_chk :
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tacval com :
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Chk.tac ->
Tactic.Syn.tac