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

7 files changed, 142 insertions, 75 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e9e1882f87..0c25e0ff88 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -50,10 +50,12 @@ type refiner_error =
 
 exception RefinerError of refiner_error
 
+open Pretype_errors
+
 let catchable_exception = function
   | Util.UserError _ | TypeError _ | RefinerError _
   | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
-    Nametab.GlobalizationError _)) -> true
+    Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
   | _ -> false
 
 let error_cannot_unify (m,n) =
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 6f4cf46408..b905c0a26b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -18,6 +18,8 @@ open Util
 open Tacexpr
 open Rawterm
 open Genarg
+open Nametab
+open Pattern
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
@@ -67,31 +69,33 @@ and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
 type hyp_location = identifier Tacexpr.raw_hyp_location
 
-type open_generic_argument =
-    (constr,raw_tactic_expr) generic_argument
-type closed_generic_argument =
-    (constr,raw_tactic_expr) generic_argument
-
-type 'a closed_abstract_argument_type =
-    ('a,constr,raw_tactic_expr) abstract_argument_type
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index bf5d4f316d..9337408824 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -18,6 +18,8 @@ open Util
 open Tacexpr
 open Rawterm
 open Genarg
+open Nametab
+open Pattern
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
@@ -95,31 +97,32 @@ and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
   (constr,
+   constr_pattern,
    evaluable_global_reference,
    inductive or_metanum,
-   identifier)
+   ltac_constant,
+   identifier,
+   glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
 type hyp_location = identifier Tacexpr.raw_hyp_location
-
-type open_generic_argument =
-    (constr,raw_tactic_expr) generic_argument
-type closed_generic_argument =
-    (constr,raw_tactic_expr) generic_argument
-
-type 'a closed_abstract_argument_type =
-    ('a,constr,raw_tactic_expr) abstract_argument_type
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 61fc3f3b1d..01787f7d96 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -856,7 +856,7 @@ open Pp
 
 let pr_tactic = function
   | Tacexpr.TacArg (Tacexpr.Tacexp t) ->
-      Pptactic.pr_raw_tactic t (*top tactic from tacinterp*)
+      Pptactic.pr_glob_tactic t (*top tactic from tacinterp*)
   | t -> Pptactic.pr_tactic t
 
 let pr_rule = function
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 146d4bd293..a2584773f2 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -15,6 +15,7 @@ open Nametab
 open Rawterm
 open Util
 open Genarg
+open Pattern
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
@@ -29,6 +30,9 @@ type raw_red_flag =
 
 type raw_red_expr = (constr_expr, reference or_metanum) red_expr_gen
 
+type glob_red_expr =
+    (rawconstr_and_expr, evaluable_global_reference or_var or_metanum) red_expr_gen
+
 let make_red_flag =
   let rec add_flag red = function
     | [] -> red
@@ -86,7 +90,7 @@ type ('a,'t) match_rule =
   | Pat of 'a match_context_hyps list * 'a match_pattern * 't
   | All of 't
 
-type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
+type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of intro_pattern_expr list
   | TacIntrosUntil of quantified_hypothesis
@@ -122,9 +126,6 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   | TacDecomposeAnd of 'constr
   | TacDecomposeOr of 'constr
   | TacDecompose of 'ind list * 'constr
-(*
-  | TacOldElim of 'constr
-*)
   | TacSpecialize of int option * 'constr with_bindings
   | TacLApply of 'constr
 
@@ -147,7 +148,7 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   | TacLeft of 'constr substitution
   | TacRight of 'constr substitution
   | TacSplit of bool * 'constr substitution
-  | TacAnyConstructor of raw_tactic_expr option
+  | TacAnyConstructor of 'tac option
   | TacConstructor of int or_metaid * 'constr substitution
 
   (* Conversion *)
@@ -161,76 +162,130 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* For ML extensions *)
-  | TacExtend of loc * string * ('constr,raw_tactic_expr) generic_argument list
+  | TacExtend of loc * string * ('constr,'tac) generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of string *
-      (identifier * ('constr,raw_tactic_expr) generic_argument) list
-      * raw_tactic_expr
-
-and raw_tactic_expr =
-    (constr_expr,reference or_metanum,reference or_metanum,identifier located or_metaid) gen_tactic_expr
-
-and ('constr,'cst,'ind,'id) gen_tactic_expr =
-  | TacAtom of loc * ('constr,'cst,'ind,'id) gen_atomic_tactic_expr
-  | TacThen of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacThens of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr list
-  | TacFirst of ('constr,'cst,'ind,'id) gen_tactic_expr list
-  | TacSolve of ('constr,'cst,'ind,'id) gen_tactic_expr list
-  | TacTry of ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacOrelse of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacDo of int * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacRepeat of ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacProgress of ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacAbstract of ('constr,'cst,'ind,'id) gen_tactic_expr * identifier option
+      (identifier * ('constr,'tac) generic_argument) list
+      * 'tac
+
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
+  | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
+  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacDo of int * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
   | TacId
   | TacFail of int * string
-  | TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr
+  | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
 
-  | TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacLetIn of (identifier located * constr_expr may_eval option * ('constr,'cst,'ind,'id) gen_tactic_arg) list * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacLetCut of (identifier * constr_expr may_eval * ('constr,'cst,'ind,'id) gen_tactic_arg) list
-  | TacMatch of constr_expr may_eval * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
-  | TacMatchContext of direction_flag * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
-  | TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast
-  | TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg
+  | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacLetIn of (identifier located * ('constr,'cst) may_eval option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacLetCut of (identifier * ('constr,'cst) may_eval * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list
+  | TacMatch of ('constr,'cst) may_eval * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
+  | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
 
-and ('constr,'cst,'ind,'id) gen_tactic_fun_ast =
-  identifier option list * ('constr,'cst,'ind,'id) gen_tactic_expr
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
+  identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
 
   (* These are possible arguments of a tactic definition *)
-and ('constr,'cst,'ind,'id) gen_tactic_arg =
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
-  | MetaNumArg     of loc * int
   | MetaIdArg      of loc * string
-  | ConstrMayEval  of 'constr may_eval
-  | Reference      of reference
+  | ConstrMayEval  of ('constr,'cst) may_eval
+  | Identifier     of identifier (* parsed under Reference (Ident _) *)
+  | Reference      of 'ref
   | Integer        of int
   | TacCall        of loc *
-      reference * ('constr,'cst,'ind,'id) gen_tactic_arg list
-  | Tacexp of raw_tactic_expr
+      'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+  | Tacexp of 'tac
+
+type raw_tactic_expr =
+    (constr_expr,
+     pattern_expr,
+     reference or_metanum,
+     reference or_metanum,
+     reference,
+     identifier located or_metaid,
+     raw_tactic_expr) gen_tactic_expr
 
 type raw_atomic_tactic_expr =
-    (constr_expr,                 (* constr *)
-     reference or_metanum,        (* evaluable reference *)
-     reference or_metanum,        (* inductive *)
-     identifier located or_metaid (* identifier *)
-    ) gen_atomic_tactic_expr
+    (constr_expr,                  (* constr *)
+     pattern_expr,                 (* pattern *)
+     reference or_metanum,         (* evaluable reference *)
+     reference or_metanum,         (* inductive *)
+     reference,                    (* ltac reference *)
+     identifier located or_metaid, (* identifier *)
+     raw_tactic_expr) gen_atomic_tactic_expr
 
 type raw_tactic_arg =
     (constr_expr,
+     pattern_expr,
      reference or_metanum,
      reference or_metanum,
-     identifier located or_metaid) gen_tactic_arg
+     reference,
+     identifier located or_metaid,
+     raw_tactic_expr) gen_tactic_arg
 
 type raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
+(* Globalized tactics *)
+type glob_tactic_expr =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var or_metanum,
+     inductive or_var or_metanum,
+     ltac_constant or_var,
+     identifier located,
+     glob_tactic_expr) gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var or_metanum,
+     inductive or_var or_metanum,
+     ltac_constant or_var,
+     identifier located,
+     glob_tactic_expr) gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var or_metanum,
+     inductive or_var or_metanum,
+     ltac_constant or_var,
+     identifier located,
+     glob_tactic_expr) gen_tactic_arg
+
+type glob_generic_argument =
+    (rawconstr_and_expr,glob_tactic_expr) generic_argument
+
 type closed_raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
 type 'a raw_abstract_argument_type =
-    ('a, constr_expr,raw_tactic_expr) abstract_argument_type
+    ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+
+type 'a glob_abstract_argument_type =
+    ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+
+type open_generic_argument =
+    (Term.constr,glob_tactic_expr) generic_argument
+
+type closed_generic_argument =
+    (Term.constr,glob_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+    ('a,Term.constr,glob_tactic_expr) abstract_argument_type
 
 type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 9c0b77f581..42bbb86372 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -40,7 +40,7 @@ let help () =
 let goal_com g tac_ast =
   begin
     db_pr_goal g;
-    msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++
+    msg (str "Going to execute:" ++ fnl () ++ (pr_glob_tactic tac_ast) ++
          fnl ())
   end
 
@@ -114,7 +114,8 @@ let db_pattern_rule debug num r =
   if debug = DebugOn then
   begin
     msgnl (str "Pattern rule " ++ int num ++ str ":");
-    msgnl (str "|" ++ spc () ++ pr_match_rule false pr_raw_tactic r)
+    msgnl (str "|" ++ spc () ++ 
+      pr_match_rule false Printer.pr_pattern pr_glob_tactic r)
   end
 
 (* Prints the hypothesis pattern identifier if it exists *)
@@ -150,7 +151,9 @@ let db_hyp_pattern_failure debug env hyp =
   if debug = DebugOn then
     msgnl (str ("The pattern hypothesis"^(hyp_bound (fst hyp))^
                 " cannot match: ") ++
-           pr_match_pattern (pp_match_pattern env (snd hyp)))
+           pr_match_pattern
+             (Printer.pr_pattern_env env (names_of_rel_context env))
+             (snd hyp))
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 82f01f461b..f859b31dd4 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -27,14 +27,14 @@ type debug_info =
 
 (* Prints the state and waits *)
 val debug_prompt :
-  goal sigma -> debug_info -> Tacexpr.raw_tactic_expr -> debug_info
+  goal sigma -> debug_info -> Tacexpr.glob_tactic_expr -> debug_info
 
 (* Prints a constr *)
 val db_constr : debug_info -> env -> constr -> unit
 
 (* Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (pattern_expr,raw_tactic_expr) match_rule -> unit
+  debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :