Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; fusion NoHypId et Hyp

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

3 files changed, 9 insertions, 9 deletions

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3461987c42..2adc93ee50 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -82,8 +82,7 @@ type 'a match_pattern =
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
-  | NoHypId of 'a match_pattern
-  | Hyp of identifier located * 'a match_pattern
+  | Hyp of name located * 'a match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type ('a,'t) match_rule =
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 42bbb86372..3802f022cc 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 open Ast
+open Names
 open Constrextern
 open Pp
 open Pptactic
@@ -120,8 +121,8 @@ let db_pattern_rule debug num r =
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
-  | None -> " (unbound)"
-  | Some id -> " (bound to "^(Names.string_of_id id)^")"
+  | Anonymous -> " (unbound)"
+  | Name id -> " (bound to "^(Names.string_of_id id)^")"
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) ido =
@@ -147,13 +148,13 @@ let pp_match_pattern env = function
     Subterm (o,(extern_pattern env (names_of_rel_context env) c))
 
 (* Prints a failure message for an hypothesis pattern *)
-let db_hyp_pattern_failure debug env hyp =
+let db_hyp_pattern_failure debug env (na,hyp) =
   if debug = DebugOn then
-    msgnl (str ("The pattern hypothesis"^(hyp_bound (fst hyp))^
+    msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            pr_match_pattern
              (Printer.pr_pattern_env env (names_of_rel_context env))
-             (snd hyp))
+             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 f859b31dd4..c847534c4a 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -38,7 +38,7 @@ val db_pattern_rule :
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> identifier * constr -> identifier option -> unit
+  debug_info -> env -> identifier * constr -> name -> unit
 
 (* Prints the matched conclusion *)
 val db_matched_concl : debug_info -> env -> constr -> unit
@@ -48,7 +48,7 @@ val db_mc_pattern_success : debug_info -> unit
 
 (* Prints a failure message for an hypothesis pattern *)
 val db_hyp_pattern_failure :
-  debug_info -> env -> identifier option * constr_pattern match_pattern -> unit
+  debug_info -> env -> name * constr_pattern match_pattern -> unit
 
 (* Prints a matching failure message for a rule *)
 val db_matching_failure : debug_info -> unit