summaryrefslogtreecommitdiff
path: root/proofs/evar_refiner.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.mli')
-rw-r--r--proofs/evar_refiner.mli41
1 files changed, 5 insertions, 36 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index d57e1b84..9880f2f0 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,52 +6,21 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evar_refiner.mli,v 1.28.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
(*i*)
open Names
open Term
-open Sign
open Environ
open Evd
open Refiner
-open Proof_type
(*i*)
-type wc = named_context sigma (* for a better reading of the following *)
-
(* Refinement of existential variables. *)
-val rc_of_pfsigma : proof_tree sigma -> wc
-val rc_of_glsigma : goal sigma -> wc
-
-(* 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
- dependent goal *)
-type w_tactic = wc -> wc
-
-val startWalk : goal sigma -> wc * (wc -> tactic)
-
-val extract_decl : evar -> w_tactic
-val restore_decl : evar -> evar_info -> w_tactic
-val w_Declare : evar -> types -> w_tactic
-val w_Define : evar -> constr -> w_tactic
-
-val w_Underlying : wc -> evar_map
-val w_env : wc -> env
-val w_hyps : wc -> named_context
-val w_whd : wc -> constr -> constr
-val w_type_of : wc -> constr -> constr
-val w_add_sign : (identifier * types) -> w_tactic
+val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
-val w_whd_betadeltaiota : wc -> constr -> constr
-val w_hnf_constr : wc -> constr -> constr
-val w_conv_x : wc -> constr -> constr -> bool
-val w_const_value : wc -> constant -> constr
-val w_defined_evar : wc -> existential_key -> bool
+val instantiate_pf_com :
+ int -> Topconstr.constr_expr -> pftreestate -> pftreestate
-val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic
-(*i
-val instantiate_tac : tactic_arg list -> tactic
-i*)
-val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)