'status * (NReference.reference * int * NCic.term list * NCic.term list * NCic.constructor list)
val ppterm: #pstatus -> cic_term -> string
val ppcontext: #pstatus -> NCic.context -> string
val whd:
'status * (NReference.reference * int * NCic.term list * NCic.term list * NCic.constructor list)
val ppterm: #pstatus -> cic_term -> string
val ppcontext: #pstatus -> NCic.context -> string
val whd:
- #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
-val metas_of_term : #pstatus as 'status -> cic_term -> int list
+ (#pstatus as 'status) -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
+val metas_of_term : (#pstatus as 'status) -> cic_term -> int list
-val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
-val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
+val instantiate: (#pstatus as 'status) -> ?refine:bool -> int -> cic_term -> 'status
+val instantiate_with_ast: (#pstatus as 'status) -> int -> tactic_term -> 'status
found: ('status -> cic_term -> 'status * cic_term) ->
postprocess: ('status -> cic_term -> 'status * cic_term) ->
cic_term -> tactic_term option * NCic.term ->
'status * cic_term
found: ('status -> cic_term -> 'status * cic_term) ->
postprocess: ('status -> cic_term -> 'status * cic_term) ->
cic_term -> tactic_term option * NCic.term ->
'status * cic_term
class type virtual tac_status = [Continuationals.Stack.t] status
val pp_tac_status: #tac_status -> unit
class type virtual tac_status = [Continuationals.Stack.t] status
val pp_tac_status: #tac_status -> unit