moved instantiate binding to extratactics

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

4 files changed, 28 insertions, 30 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 21f5a7368..126e35663 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -111,21 +111,31 @@ let make_rule loc (prods,act) =
   <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >>
 
 let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
-  let interp = match f with
-    | None -> <:expr< Tacinterp.interp_genarg >>
-    | Some f -> <:expr< $lid:f$>> in
-  let glob = match g with
-    | None -> <:expr< Tacinterp.intern_genarg >>
-    | Some f -> <:expr< $lid:f$>> in
-  let substitute = match h with
-    | None -> <:expr< Tacinterp.subst_genarg >>
-    | Some f -> <:expr< $lid:f$>> in
   let rawtyp, rawpr = match rawtyppr with
     | None -> typ,pr
     | Some (t,p) -> t,p in
   let globtyp, globpr = match globtyppr with
     | None -> typ,pr
     | Some (t,p) -> t,p in
+  let glob = match g with
+    | None ->
+	<:expr< fun e x ->
+          out_gen $make_globwit loc typ$
+            (Tacinterp.intern_genarg e
+               (in_gen $make_rawwit loc rawtyp$ x)) >>
+    | Some f -> <:expr< $lid:f$>> in
+  let interp = match f with
+    | None -> 
+	<:expr< fun ist gl x ->
+          out_gen $make_wit loc typ$
+            (Tacinterp.interp_genarg ist gl (in_gen $make_globwit loc globtyp$ x)) >>
+    | Some f -> <:expr< $lid:f$>> in
+  let substitute = match h with
+    | None -> 
+	<:expr< fun s x ->
+          out_gen $make_globwit loc globtyp$
+	    (Tacinterp.subst_genarg s (in_gen $make_globwit loc globtyp$ x)) >>
+    | Some f -> <:expr< $lid:f$>> in
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
@@ -138,23 +148,11 @@ let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl =
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
       Tacinterp.add_interp_genarg $se$
         ((fun e x ->
-          (in_gen $globwit$
-             (out_gen $make_globwit loc typ$
-          	($glob$ e
-         	  (in_gen $make_rawwit loc rawtyp$
-	             (out_gen $rawwit$ x)))))),
+          (in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
         (fun ist gl x ->
-          (in_gen $wit$
-             (out_gen $make_wit loc typ$
-          	($interp$ ist gl
-         	  (in_gen $make_globwit loc rawtyp$
-	             (out_gen $globwit$ x)))))),
+          (in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))),
         (fun subst x ->
-          (in_gen $globwit$
-             (out_gen $make_globwit loc typ$
-          	($substitute$ subst
-         	  (in_gen $make_globwit loc rawtyp$
-	             (out_gen $globwit$ x)))))));
+          (in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
       Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
         [(None, None, $rules$)];
       Pptactic.declare_extra_genarg_pprule
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 22a1fc2df..db11026a4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -303,10 +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 -> 
+(*    | 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))
+	    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 16811ff85..ae052f462 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -347,12 +347,12 @@ 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; ")"; "in";
+    (*  | 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 ())
+            TacInstantiate (n,c,ConclLocation ()) *)
 
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f334dd633..36440088c 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -496,12 +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,ConclLocation ()) ->
+ (* | 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)