From 77b37b73d711af9b0725f1d63f99ad3157486cbb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Jun 2002 14:34:22 +0000
Subject: Ajout coercion constr vers hyp quantifiée

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e0a573d642..9609bb49f9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1047,11 +1047,8 @@ let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id -> 
       match eval_ident ist id with
-	| VIdentifier id -> NamedHyp id
 	| VInteger n -> AnonHyp n
-	| _ -> invalid_arg_loc
-	    (loc, "Not a reference to an hypothesis: "^(string_of_id id))
-
+	| v -> NamedHyp (coerce_to_hypothesis ist v)
 
 let interp_induction_arg ist = function
   | ElimOnConstr c -> ElimOnConstr (constr_interp ist c)
@@ -1389,7 +1386,8 @@ and vcontext_interp ist = function
   | (VContext (ist',lr,lmr)) as v ->
     (match ist.goalopt with
     | None -> v
-    | Some g -> match_context_interp ist lr lmr g)
+    | Some g ->
+        match_context_interp ist lr lmr g)
 (* The closure system does not work yet. It must be better studied. *)
 (* (* Relaunch *) match_context_interp ist' lr lmr g)*)
   | v -> v
-- 
cgit v1.2.3