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, 11 insertions, 9 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 56abfb82b5..e1b8e7125e 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -239,9 +239,9 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
    by the list of integers given as extra arguments.
  *)
 
-let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
-let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level
-let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level
+let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
+let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level
+let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level
 
 
 let on_then = function [t1;t2;l] ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 585e4bfb65..ecb04e0755 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -682,7 +682,7 @@ let xlate_with_names = function
     IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
   | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
 
-let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
+let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
 
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
   function
@@ -1271,14 +1271,15 @@ and coerce_genarg_to_TARG x =
       (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType n ->
-      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
-      CT_coerce_TACTIC_COM_to_TARG t
   | OpenConstrArgType b -> 
       CT_coerce_SCOMMENT_CONTENT_to_TARG
       	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
+  | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
+      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
+      CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1368,8 +1369,9 @@ let coerce_genarg_to_VARG x =
       (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType n ->
-      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
+  | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
+      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"