more evar stuff

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 10 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ae9fc2aedb..22a1fc2dfa 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -303,8 +303,10 @@ GEXTEND Gram
       | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
       | IDENT "LetTac"; (_,na) = name; ":="; c = constr; p = clause_pattern
         -> TacLetTac (na,c,p)
-      | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> 
-	    TacInstantiate (n,c,cls)
+      | IDENT "Instantiate"; n = natural; c = constr -> 
+	    TacInstantiate (n,c,ConclLocation ())
+      | IDENT "Instantiate"; n = natural; c = constr; "in"; id = id_or_meta -> 
+	    TacInstantiate (n,c,HypLocation(id,InHypTypeOnly))
       | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
       | IDENT "LApply"; c = constr -> TacLApply c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index e307f96f9e..16811ff853 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -347,10 +347,13 @@ GEXTEND Gram
           p = clause -> TacLetTac (Names.Name id,c,p)
       | IDENT "set"; c = constr; p = clause ->
           TacLetTac (Names.Anonymous,c,p)
-      | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
-	  cls = clause ->
-            TacInstantiate (n,c,cls)
-	    
+      | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; "in";
+	  hid = hypident ->
+	    let (id,(hloc,_)) = hid in
+              TacInstantiate (n,c,HypLocation (id,hloc))
+      | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" ->
+            TacInstantiate (n,c,ConclLocation ())
+
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
       | IDENT "lapply"; c = constr -> TacLApply c
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index cd31b7f264..f334dd6338 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -154,7 +154,6 @@ let pr_clause pr_id = function
   | [] -> mt ()
   | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
 
-
 let pr_clauses pr_id cls =
   match cls with
       { onhyps = Some l; onconcl = false } ->
@@ -497,9 +496,12 @@ and pr_atom1 = function
         | _ -> pr_clauses pr_ident cl in
       hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
              pr_constr c ++ pcl)
-  | TacInstantiate (n,c,cls) ->
-      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
-	     pr_clauses pr_ident cls)
+  | TacInstantiate (n,c,ConclLocation ()) ->
+      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c )
+  | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
+	     str "in" ++  pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+
   (* Derived basic tactics *)
   | TacSimpleInduction (h,_) ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)