diff options
Diffstat (limited to 'proofs/evar_refiner.mli')
| -rw-r--r-- | proofs/evar_refiner.mli | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 9f09cfba5..4138a49c3 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -32,7 +32,6 @@ val rc_of_glsigma : goal sigma -> named_context sigma hyps : context of the goal; decls : a superset of evars of which the goal may depend })] *) -type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a (* A [w_tactic] is a tactic which modifies the a set of evars of which a goal depend, either by instantiating one, or by declaring a new @@ -45,10 +44,12 @@ val local_Constraints : val startWalk : goal sigma -> named_context sigma * (named_context sigma -> tactic) -val walking_THEN : 'a result_w_tactic -> ('a -> tactic) -> tactic -val walking : w_tactic -> tactic -val w_Focusing_THEN : - evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic +val extract_decl : evar -> named_context sigma -> named_context sigma + +val restore_decl : evar -> evar_info -> named_context sigma -> named_context sigma + +(* val w_Focusing_THEN : + evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic *) val w_Declare : evar -> types -> w_tactic val w_Define : evar -> constr -> w_tactic @@ -61,9 +62,6 @@ val w_type_of : named_context sigma -> constr -> constr val w_add_sign : (identifier * types) -> named_context sigma -> named_context sigma -val w_IDTAC : w_tactic -val w_ORELSE : w_tactic -> w_tactic -> w_tactic -val ctxt_type_of : named_context sigma -> constr -> constr val w_whd_betadeltaiota : named_context sigma -> constr -> constr val w_hnf_constr : named_context sigma -> constr -> constr val w_conv_x : named_context sigma -> constr -> constr -> bool @@ -71,5 +69,6 @@ val w_const_value : named_context sigma -> constant -> constr val w_defined_const : named_context sigma -> constant -> bool val w_defined_evar : named_context sigma -> existential_key -> bool -val instantiate_pf : int -> constr -> pftreestate -> pftreestate +val instantiate : evar -> constr -> tactic +val instantiate_tac : tactic_arg list -> tactic val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate |