Globalisation des noms de tactiques dans les définitions de tactiques

pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).


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

1 files changed, 28 insertions, 31 deletions

diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index a3d5f496e..a7da88b52 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -11,6 +11,7 @@
 open Genarg
 open Q_util
 open Q_coqast
+open Argextend
 
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 let loc = (0,0)
@@ -35,35 +36,19 @@ let rec make_when loc = function
       <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
   | _::l -> make_when loc l
 
-let rec make_wit loc = function
-  | BoolArgType -> <:expr< Genarg.wit_bool >>
-  | IntArgType -> <:expr< Genarg.wit_int >>
-  | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
-  | StringArgType -> <:expr< Genarg.wit_string >>
-  | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
-  | IdentArgType -> <:expr< Genarg.wit_ident >>
-  | RefArgType -> <:expr< Genarg.wit_ref >>
-  | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
-  | SortArgType -> <:expr< Genarg.wit_sort >>
-  | ConstrArgType -> <:expr< Genarg.wit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
-  | TacticArgType -> <:expr< Genarg.wit_tactic >>
-  | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
-  | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
-  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
-  | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
-  | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
-  | PairArgType (t1,t2) -> 
-      <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
-  | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >>
-
 let rec make_let e = function
   | [] -> e
   | TacNonTerm(loc,t,_,Some p)::l ->
       let loc = join_loc loc (MLast.loc_of_expr e) in
       let e = make_let e l in
-      <:expr< let $lid:p$ = Genarg.out_gen $make_wit loc t$ $lid:p$ in $e$ >>
+      let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
+      let v = 
+        (* Special case for tactics which must be stored in algebraic
+           form to avoid marshalling closures and to be reprinted *)
+        if t = TacticArgType then
+          <:expr< ($v$, Tacinterp.eval_tactic $v$) >>
+        else v in
+      <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let e l
 
 let add_clause s (_,pt,e) l =
@@ -95,6 +80,16 @@ let rec make_args = function
       <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
   | _::l -> make_args l
 
+let rec make_eval_tactic e = function
+  | [] -> e
+  | TacNonTerm(loc,TacticArgType,_,Some p)::l ->
+      let loc = join_loc loc (MLast.loc_of_expr e) in
+      let e = make_eval_tactic e l in
+        (* Special case for tactics which must be stored in algebraic
+           form to avoid marshalling closures and to be reprinted *)
+      <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >>
+  | _::l -> make_eval_tactic e l
+
 let rec make_fun e = function
   | [] -> e
   | TacNonTerm(loc,_,_,Some p)::l -> 
@@ -142,7 +137,7 @@ let declare_tactic_v7 loc s cl =
     let e = 
       make_fun
         <:expr<
-          Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $e$
+          Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$
         >>
       p in
     <:str_item< value $lid:stac$ = $e$ >>
@@ -153,7 +148,7 @@ let declare_tactic_v7 loc s cl =
       open Pcoq;
       Egrammar.extend_tactic_grammar $se$ $gl$;
       let pp = fun [ $list:pl$ ] in
-      Pptactic.declare_extra_tactic_pprule False $se$ pp pp;
+      Pptactic.declare_extra_tactic_pprule False $se$ pp;
     end
   >>
 
@@ -170,25 +165,26 @@ let declare_tactic loc s cl =
     let e = 
       make_fun
         <:expr<
-          Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $e$
+          Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $make_eval_tactic e p$
         >>
       p in
     <:str_item< value $lid:stac$ = $e$ >>
   in
+  let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
   let se = mlexpr_of_string s in
   <:str_item<
     declare
       open Pcoq;
-      declare $list:List.map hide_tac cl'$ end;
+      declare $list:hidden$ end;
       try
        Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ])
       with e -> Pp.pp (Cerrors.explain_exn e);
       Egrammar.extend_tactic_grammar $se'$ $gl'$;
       let pp' = fun [ $list:pl'$ ] in
-      Pptactic.declare_extra_tactic_pprule True $se'$ pp' pp';
+      Pptactic.declare_extra_tactic_pprule True $se'$ pp';
       Egrammar.extend_tactic_grammar $se'$ $gl$;
       let pp = fun [ $list:pl$ ] in
-      Pptactic.declare_extra_tactic_pprule False $se'$ pp pp;
+      Pptactic.declare_extra_tactic_pprule False $se'$ pp;
     end
   >>
 
@@ -206,7 +202,8 @@ let rec interp_entry_name loc s =
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
     let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
-  else 
+  else
+    
     let t, se =
       match Pcoq.entry_type (Pcoq.get_univ "prim") s with
 	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>