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

13 files changed, 114 insertions, 146 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8831b054b5..ce671515f9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -471,12 +471,17 @@ let internalise isarity sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern false env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
-    | CPatVar (loc, n) when allow_soapp = None or !interning_grammar ->
+    | CPatVar (loc, n) when allow_soapp = None ->
 	RPatVar (loc, n)
+    | CPatVar (loc, n) when Options.do_translate () ->
+	RVar (loc, snd n)
     | CPatVar (loc, (false,n as x)) ->
-        if List.mem n (out_some allow_soapp) then 
+        if List.mem n (out_some allow_soapp) or Options.do_translate () then
 	  RPatVar (loc, x)
-        else 
+        else if List.mem n (fst (let (a,_,_) = lvar in a))
+	  (* & !Options.v7 : ne pas exiger, Tauto est encore en V7 ! *) then 
+	  RVar (loc, n)
+	else
           error_unbound_patvar loc n
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index a0bd0fb5ec..88d108fdde 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -179,7 +179,10 @@ GEXTEND Gram
       | s=sort -> CSort(loc,s)
       | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
       | IDENT "_" -> CHole loc
+(*
       | "?"; n=Prim.natural -> CPatVar(loc,(false,Pattern.patvar_of_int n)) ] ]
+*)
+      | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
     [ [ kw=fix_kw; dcl=fix_decl ->
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index fb6e213a40..b299a33680 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -98,12 +98,12 @@ GEXTEND Gram
   (* Either an hypothesis or a ltac ref (variable or pattern patvar) *)
   id_or_ltac_ref:
     [ [ id = base_ident -> AN id
-      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ]
+(*      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ]
   ;
   (* Either a global ref or a ltac ref (variable or pattern patvar) *)
   global_or_ltac_ref:
     [ [ qid = global -> AN qid
-      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ]
+(*      | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ]
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 773f97c667..5e27f9ca8c 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -307,7 +307,7 @@ let parse_226_tail tk = parser
       TokIdent (get_buff len)
 
 
-(* Parse what foolows a dot *)
+(* Parse what follows a dot *)
 let parse_after_dot bp c strm =
   if !Options.v7 then 
     match strm with parser
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8e6d63c2d6..0f26e390b8 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -183,8 +183,7 @@ let pr_match_pattern pr_pat = function
   | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
-  | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp
-  | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr_pat pr = function
   | Pat ([],mp,t) when m ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 495e2eaffe..bb0164962c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -305,9 +305,8 @@ let mlexpr_of_match_pattern = function
       <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
 
 let mlexpr_of_match_context_hyps = function
-  | Tacexpr.NoHypId l -> <:expr< Tacexpr.NoHypId $mlexpr_of_match_pattern l$ >>
   | Tacexpr.Hyp (id,l) ->
-      let f = mlexpr_of_located mlexpr_of_ident in
+      let f = mlexpr_of_located mlexpr_of_name in
       <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >>
 
 let mlexpr_of_match_rule f = function
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5ad06a6e52..0a3f6d995a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -21,7 +21,7 @@ open Pp
 (* Metavariables *)
 
 type patvar_map = (patvar * constr) list
-let patvar_of_int n = Names.id_of_string (string_of_int n)
+let patvar_of_int n = Names.id_of_string ("X" ^ string_of_int n)
 let pr_patvar = pr_id
 
 (* Patterns *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f94c14e71f..0e76558f1f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -228,7 +228,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       assert (not someta);
       let j =
 	try
-	  List.assoc n lmeta
+	  List.assoc n (lmeta@lvar)
 	with
             Not_found ->
 	      user_err_loc
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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ea7765cd62..b065aac186 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -348,7 +348,8 @@ let error_unbound_metanum loc n =
   (loc,"intern_qualid_or_metanum", str "?" ++ pr_patvar n ++ str " is unbound")
 
 let intern_metanum sign loc n =
-  if List.mem n sign.metavars then n else error_unbound_metanum loc n
+  if List.mem n sign.metavars or find_var n sign then n
+  else error_unbound_metanum loc n
 
 let intern_hyp_or_metanum ist = function
   | AN id -> AN (intern_hyp ist (loc,id))
@@ -524,14 +525,10 @@ let intern_constr_may_eval ist = function
 
 (* Reads the hypotheses of a Match Context rule *)
 let rec intern_match_context_hyps evc env lfun = function
-  | (NoHypId mp)::tl ->
+  | (Hyp ((_,na) as locna,mp))::tl ->
       let metas1, pat = intern_pattern evc env lfun mp in
       let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in
-      lfun, metas1@metas2, (NoHypId pat)::hyps
-  | (Hyp ((_,s) as locs,mp))::tl ->
-      let metas1, pat = intern_pattern evc env lfun mp in
-      let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in
-      s::lfun, metas1@metas2, Hyp (locs,pat)::hyps
+      name_fold (fun a l -> a::l) na lfun, metas1@metas2, Hyp (locna,pat)::hyps
   | [] -> lfun, [], []
 
 (* Utilities *)
@@ -753,7 +750,7 @@ and intern_match_rule ist = function
       let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
       let metas2,pat = intern_pattern sigma env lfun mp in
       let metas = list_uniquize (metas1@metas2@lmeta) in
-      let ist' = { ist with ltacvars = (lfun',l2); metavars = metas } in
+      let ist' = { ist with ltacvars = (metas@lfun',l2); metavars = [] } in
       Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
   | [] -> []
 
@@ -834,18 +831,18 @@ let read_pattern evc env lfun = function
   | Term pc -> Term (eval_pattern lfun pc)
 
 (* Reads the hypotheses of a Match Context rule *)
-let rec read_match_context_hyps evc env lfun lidh = function
-  | (NoHypId mp)::tl ->
-    (NoHypId (read_pattern evc env lfun mp))::
-      (read_match_context_hyps evc env lfun lidh tl)
-  | (Hyp ((loc,id) as locid,mp))::tl ->
-    if List.mem id lidh then
-      user_err_loc (loc,"Tacinterp.read_match_context_hyps",
+let cons_and_check_name id l =
+  if List.mem id l then
+    user_err_loc (loc,"read_match_context_hyps",
       str ("Hypothesis pattern-matching variable "^(string_of_id id)^
-           " used twice in the same pattern"))
-    else
-    (Hyp (locid,read_pattern evc env lfun mp))::
-      (read_match_context_hyps evc env lfun (id::lidh) tl)
+      " used twice in the same pattern"))
+  else id::l
+
+let rec read_match_context_hyps evc env lfun lidh = function
+  | (Hyp ((loc,na) as locna,mp))::tl ->
+      let lidh' = name_fold cons_and_check_name na lidh in
+      Hyp (locna,read_pattern evc env lfun mp)::
+	(read_match_context_hyps evc env lfun lidh' tl)
   | [] -> []
 
 (* Reads the rules of a Match Context or a Match *)
@@ -887,69 +884,40 @@ let apply_matching pat csr =
      PatternMatchingFailure -> raise No_match
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt =
-  let get_pattern = function
-    | Hyp (_,pat) -> pat
-    | NoHypId pat -> pat
-  and get_id_couple id = function
-    | Hyp((_,idpat),_) -> [idpat,VIdentifier id]
-    | NoHypId _ -> [] 
-  and get_info_pattern = function
-    | Hyp((_,idpat),pat) -> (Some idpat,pat)
-    | NoHypId pat -> (None,pat) in
-  let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function
-    | (id,hyp)::tl ->
-      (match (get_pattern mhyp) with
+let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) =
+  let get_id_couple id = function
+    | Name idpat -> [idpat,VIdentifier id]
+    | Anonymous -> [] in
+  let rec apply_one_mhyp_context_rec nocc = function
+    | (id,hyp)::tl as hyps ->
+      (match pat with
       | Term t ->
         (try
-          let lmeta = 
-            verify_metas_coherence gl lmatch (matches t hyp) in
-          (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
-         with | PatternMatchingFailure | Not_coherent_metas ->
-          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl)
+          let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
+          (get_id_couple id hypname,lmeta,(id,hyp),(tl,0))
+        with
+	| PatternMatchingFailure | Not_coherent_metas ->
+            apply_one_mhyp_context_rec 0 tl)
       | Subterm (ic,t) ->
         (try
           let (lm,ctxt) = sub_match nocc t hyp in
           let lmeta = verify_metas_coherence gl lmatch lm in
-          (get_id_couple id mhyp,give_context ctxt
-            ic,lmeta,tl,(id,hyp),Some nocc)
+          ((get_id_couple id hypname)@(give_context ctxt ic),
+	   lmeta,(id,hyp),(hyps,nocc + 1))
          with
-        | NextOccurrence _ ->
-          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl
-        | Not_coherent_metas ->
-          apply_one_mhyp_context_rec ist env mhyp lhyps_acc (nocc + 1)
-                                     ((id,hyp)::tl)))
+         | NextOccurrence _ ->
+             apply_one_mhyp_context_rec 0 tl
+         | Not_coherent_metas ->
+             apply_one_mhyp_context_rec (nocc + 1) hyps))
     | [] ->
-      begin
-        db_hyp_pattern_failure ist.debug env (get_info_pattern mhyp);
+        db_hyp_pattern_failure ist.debug env (hypname,pat);
         raise No_match
-      end in
-  let nocc =
-    match noccopt with
-    | None -> 0
-    | Some n -> n in
-  apply_one_mhyp_context_rec ist env mhyp [] nocc lhyps
-
-(* Gets the identifier of the pattern if it exists *)
-let get_id_pattern = function
-  | [] -> None
-  | [(id,_)] -> Some id
-  | _ -> assert false
-
-(*
-let coerce_to_qualid loc = function
-  | Constr c when isVar c -> make_short_qualid (destVar c)
-  | Constr c -> 
-      (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c))
-      with Not_found -> invalid_arg_loc (loc, "Not a reference"))
-  | Identifier id -> make_short_qualid id
-  | Qualid qid -> qid
-  | _ -> invalid_arg_loc (loc, "Not a reference")
-*)
+      in
+  apply_one_mhyp_context_rec nocc lhyps
 
-let constr_to_id loc c =
-  if isVar c then destVar c
-  else invalid_arg_loc (loc, "Not an identifier")
+let constr_to_id loc = function
+  | VConstr c when isVar c -> destVar c
+  | _ -> invalid_arg_loc (loc, "Not an identifier")
 
 let constr_to_qid loc c =
   try shortest_qualid_of_global Idset.empty (reference_of_constr c)
@@ -1038,7 +1006,7 @@ let eval_name ist = function
 
 let interp_hyp_or_metanum ist gl = function
   | AN id -> eval_variable ist gl (dummy_loc,id)
-  | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
+  | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lfun)
 
 (* To avoid to move to much simple functions in the big recursive block *)
 let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
@@ -1065,7 +1033,7 @@ let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
 
 let interp_inductive_or_metanum ist = function
   | MetaNum (loc,n) ->
-      coerce_to_inductive (VConstr (List.assoc n ist.lmatch))
+      coerce_to_inductive (List.assoc n ist.lfun)
   | AN r -> match r with
       | ArgArg r -> r
       | ArgVar (_,id) -> 
@@ -1073,7 +1041,7 @@ let interp_inductive_or_metanum ist = function
 
 let interp_evaluable_or_metanum ist env = function
   | MetaNum (loc,n) ->
-      coerce_to_evaluable_ref env (VConstr (List.assoc n ist.lmatch))
+      coerce_to_evaluable_ref env (List.assoc n ist.lfun)
   | AN r -> match r with
       | ArgArg (r,Some (loc,id)) ->
           (* Maybe [id] has been introduced by Intro-like tactics *)
@@ -1434,7 +1402,8 @@ and match_context_interp ist g lr lmr =
       let (lgoal,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
       if mhyps = [] then
-        eval_with_fail {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch}
+	let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
+        eval_with_fail {ist with lfun=lgoal@lctxt@ist.lfun; lmatch=ist.lmatch}
           mt goal
       else
         apply_hyps_context ist env goal mt lgoal mhyps hyps
@@ -1468,7 +1437,8 @@ and match_context_interp ist g lr lmr =
             if mhyps = [] then
             begin
               db_mc_pattern_success ist.debug;
-              eval_with_fail {ist with lmatch=lgoal@ist.lmatch} mt goal
+	      let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
+              eval_with_fail {ist with lfun=lgoal@ist.lfun} mt goal
             end
             else
               apply_hyps_context ist env goal mt lgoal mhyps hyps
@@ -1499,44 +1469,29 @@ and match_context_interp ist g lr lmr =
     (read_match_rule (project g) env (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
-  let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp
-    lhyps_rest noccopt =
-    match mhyps with
-      | hd::tl ->
-        let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
-          apply_one_mhyp_context ist env goal lmatch hd lhyps_mhyp noccopt in
-        begin
-          db_matched_hyp ist.debug (pf_env goal) hyp_match
-                         (get_id_pattern lid);
-          (try
-          if tl = [] then
-          begin
-            db_mc_pattern_success ist.debug;
-            eval_with_fail {ist with lfun=lfun@lid@lc@ist.lfun;
-                                     lmatch=lmatch@lm@ist.lmatch} mt goal
-          end
-          else
-            let nextlhyps =
-              List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
-                lhyps_rest in
-            apply_hyps_context_rec ist mt
-              (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
-           with
-           | e when is_failure e -> raise e
-	   | e when is_match_catchable e -> 
-             (match noccopt with
-             | None ->
-               apply_hyps_context_rec ist mt lfun
-                 lmatch mhyps newlhyps lhyps_rest None
-             | Some nocc ->
-               apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps
-                 (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
+and apply_hyps_context ist env goal mt (lgmatch:(Rawterm.patvar * Term.constr) list) mhyps hyps =
+  let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
+    | Hyp ((_,hypname),mhyp)::tl ->
+        let (lids,lm,hyp_match,next) =
+          apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in
+        db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
+        begin 
+	  try
+            let nextlhyps = list_except hyp_match lhyps_rest in
+            apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps
+	      (nextlhyps,0) tl
+          with
+          | e when is_failure e -> raise e
+	  | e when is_match_catchable e -> 
+	      apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps
         end
-      |	[] ->
-        anomalylabstrm "apply_hyps_context_rec" (str
-          "Empty list should not occur") in
-  apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
+    | [] ->
+	let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in
+        db_mc_pattern_success ist.debug;
+        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun;
+          lmatch=ist.lmatch} mt goal
+  in
+  apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps
 
   (* Interprets extended tactic generic arguments *)
 and interp_genarg ist goal x =
@@ -1589,7 +1544,8 @@ and match_interp ist g constr lmr =
     try 
       let (lm,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
-      val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} g mt
+      let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+      val_interp {ist with lfun=lm@lctxt@ist.lfun; lmatch=ist.lmatch} g mt
     with | NextOccurrence _ -> raise No_match
   in
   let rec apply_match ist csr = function
@@ -1598,8 +1554,10 @@ and match_interp ist g constr lmr =
          with e when is_match_catchable e -> apply_match ist csr [])
     | (Pat ([],Term c,mt))::tl ->
         (try
+	  let lm = apply_matching c csr in
+	  let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
           val_interp
-            { ist with lmatch=(apply_matching c csr)@ist.lmatch } g mt
+            { ist with lfun=lm@ist.lfun } g mt
          with e when is_match_catchable e -> apply_match ist csr tl)
     | (Pat ([],Subterm (id,c),mt))::tl ->
         (try
@@ -1853,9 +1811,6 @@ let subst_match_pattern subst = function
   | Term pc -> Term (subst_pattern subst pc)
 
 let rec subst_match_context_hyps subst = function
-  | NoHypId mp :: tl ->
-      NoHypId (subst_match_pattern subst mp)
-      :: subst_match_context_hyps subst tl
   | Hyp (locs,mp) :: tl ->
       Hyp (locs,subst_match_pattern subst mp)
       :: subst_match_context_hyps subst tl
@@ -2115,7 +2070,9 @@ let interp_redexp env evc r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ = Auto.set_extern_interp
-  (fun l -> interp_tactic {lfun=[];lmatch=l;debug=get_debug()})
+  (fun l -> 
+    let l = List.map (fun (id,c) -> (id,VConstr c)) l in
+    interp_tactic {lfun=l;lmatch=[];debug=get_debug()})
 let _ = Auto.set_extern_intern_tac 
   (fun l -> intern_tactic {(make_empty_glob_sign()) with metavars=l})
 let _ = Auto.set_extern_subst_tactic subst_tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 5a03b08413..bc746094a8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -21,28 +21,33 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Util
-   
+
+let assoc_last ist =
+  match List.assoc (Pattern.patvar_of_int 1) ist.lfun with
+    | VConstr c -> c
+    | _ -> failwith "Tauto: anomaly"
+
 let is_empty ist =
-  if (is_empty_type (List.assoc (id_of_string "1") ist.lmatch)) then
+  if is_empty_type (assoc_last ist) then
     <:tactic<Idtac>>
   else
     <:tactic<Fail>>
 
 let is_unit ist =
-  if (is_unit_type (List.assoc (id_of_string "1") ist.lmatch)) then
+  if is_unit_type (assoc_last ist) then
     <:tactic<Idtac>>
   else
     <:tactic<Fail>>
     
 let is_conj ist =
-  let ind=(List.assoc (id_of_string "1") ist.lmatch) in
+  let ind = assoc_last ist in
     if (is_conjunction ind) && (is_nodep_ind ind) then
       <:tactic<Idtac>>
     else
       <:tactic<Fail>>
 
 let is_disj ist =
-  if (is_disjunction (List.assoc (id_of_string "1") ist.lmatch)) then
+  if is_disjunction (assoc_last ist) then
     <:tactic<Idtac>>
   else
     <:tactic<Fail>>