Changement du type d'argument 'TacticArgType X' en un type

'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de
pouvoir typer correctement les wit_tactic (auparavant le typage des
wit_tactic était trop libéral et permettait de casser la
subject-reduction).

Amélioration au passage de l'affichage de la tactique "replace by" 
(module Extratactics).



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

2 files changed, 41 insertions, 36 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a6155598cd..521bf54096 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -37,54 +37,41 @@ let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
 *)
 
 (* Julien: Mise en commun des differentes version de replace with in by 
-   TODO: améliorer l'affichage et deplacer dans extraargs
+   TODO: deplacer dans extraargs
 
 *)
 
-
-let pr_by_arg_tac prc _ _ opt_c = 
+let pr_by_arg_tac _prc _prlc prtac opt_c = 
   match opt_c with 
     | None -> mt ()
-    | Some c -> spc () ++ hov 2 (str "by" ++ spc ()  )
+    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
 
 (* Julien Forest: on voudrait pouvoir passer la loc mais je 
 n'ai pas reussi 
 *)
 
-let pr_in_arg_hyp  = 
-fun prc _ _ opt_c->
+let pr_in_arg_hyp _prc _prlc _prtac opt_c =
   match opt_c with 
     | None -> mt ()
-    | Some c -> 
-	spc () ++ hov 2 (str "by" ++ spc () ++ 
-			   Pptactic.pr_or_var (fun _ -> mt ()) 
-			   (Rawterm.ArgVar(Util.dummy_loc,c))
-			)
-
-
-
+    | Some id -> spc () ++ hov 2 (str "by" ++ spc () ++ Nameops.pr_id id)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
   PRINTED BY pr_by_arg_tac
-| [ "by" tactic(c) ] -> [ Some c ]
+| [ "by" tactic3(c) ] -> [ Some c ]
 | [ ] -> [ None ]
 END
  
 ARGUMENT EXTEND in_arg_hyp
   TYPED AS ident_opt
   PRINTED BY pr_in_arg_hyp
-| [ "in" int_or_var(c) ] -> 
-    [ match c with
-	| Rawterm.ArgVar(_,c) ->  Some (c)
-	| _ -> Util.error "in must be used with an identifier" 
-    ]
+| [ "in" ident(c) ] -> [ Some (c) ]
 | [ ] -> [ None ]
 END
 
 TACTIC EXTEND replace 
-| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp)  by_arg_tac(tac)  ] ->
-    [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac)  ]
+   ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
+-> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
 (* Julien:
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20ca5dc93f..fef9ba95a0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -46,6 +46,7 @@ open Inductiveops
 open Syntax_def
 open Pretyping
 open Pretyping.Default
+open Pcoq
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
@@ -867,9 +868,6 @@ and intern_genarg ist x =
         (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n) (intern_tactic ist
-	(out_gen (rawwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
@@ -883,7 +881,14 @@ and intern_genarg ist x =
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
   | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
-  | ExtraArgType s -> lookup_genarg_glob s ist x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n) (intern_tactic ist
+	    (out_gen (rawwit_tactic n) x))
+      | None ->
+          lookup_genarg_glob s ist x
 
 (************* End globalization ************)
 
@@ -1659,7 +1664,6 @@ and interp_genarg ist goal x =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
-  | TacticArgType n -> in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
   | OpenConstrArgType casted ->
       in_gen (wit_open_constr_gen casted) 
         (pf_interp_open_constr casted ist goal 
@@ -1674,7 +1678,13 @@ and interp_genarg ist goal x =
   | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
   | OptArgType _ -> app_opt (interp_genarg ist goal) x
   | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x
-  | ExtraArgType s -> lookup_interp_genarg s ist goal x
+  | ExtraArgType s -> 
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+      | None -> 
+          lookup_interp_genarg s ist goal x
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
@@ -1879,13 +1889,17 @@ and interp_atomic ist gl = function
     | ConstrMayEvalArgType ->
 	VConstr
           (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
-    | TacticArgType n -> 
-	val_interp ist gl (out_gen (globwit_tactic n) x)
+    | ExtraArgType s when tactic_genarg_level s <> None ->
+          (* Special treatment of tactic arguments *)
+	val_interp ist gl 
+          (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
-    | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
-    | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
+    | OpenConstrArgType _ | ConstrWithBindingsArgType 
+    | ExtraArgType _ | BindingsArgType 
+    | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
+        
     in
     let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
     let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body)
@@ -2184,9 +2198,6 @@ and subst_genarg subst (x:glob_generic_argument) =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n)
-        (subst_tactic subst (out_gen (globwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
@@ -2200,7 +2211,14 @@ and subst_genarg subst (x:glob_generic_argument) =
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x
   | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
-  | ExtraArgType s -> lookup_genarg_subst s subst x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n)
+            (subst_tactic subst (out_gen (globwit_tactic n) x))
+      | None -> 
+          lookup_genarg_subst s subst x
 
 (***************************************************************************)
 (* Tactic registration *)