From ad12a2fe4c1406ea5485e2a1a4006c93f55fa676 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Sat, 26 Jun 2004 09:31:26 +0000
Subject: effective evar refining

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5827 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hiddentac.ml  | 5 +++--
 tactics/hiddentac.mli | 3 ++-
 tactics/tacinterp.ml  | 3 ++-
 3 files changed, 7 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 99fe569bb7..21f7d43fc7 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -48,8 +48,9 @@ let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
 let h_let_tac na c cl =
   abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
 let h_instantiate n c cls = 
-  abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (simple_clause_of cls))
+(Evar_refiner.instantiate n c (simple_clause_of cls))
+  (* abstract_tactic (TacInstantiate (n,c,cls))
+    (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 7c8c1b3c56..90a2d1b3c3 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -50,7 +50,8 @@ val h_generalize      : constr list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_forward         : bool -> name -> constr -> tactic 
 val h_let_tac         : name -> constr -> Tacticals.clause -> tactic
-val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
+val h_instantiate     : int -> Rawterm.rawconstr -> 
+  Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 06a4c90a75..fe557c9fcf 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1712,7 +1712,8 @@ and interp_atomic ist gl = function
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
       h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
-  | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
+  | TacInstantiate (n,c,ido) -> h_instantiate n (fst c) 
+      (* pf_interp_constr ist gl c *)
       (clause_app (interp_hyp_location ist gl) ido)
 
   (* Automation tactics *)
-- 
cgit v1.2.3