From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 proofs/evar_refiner.mli | 41 +++++------------------------------------
 1 file changed, 5 insertions(+), 36 deletions(-)

(limited to 'proofs/evar_refiner.mli')

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] *) 
-- 
cgit v1.2.3