Opened the possibility to type Ltac patterns but it is not fully functional yet

- to type patterns w/o losing the information of what subterm is a hole
  would need to remember where holes were in "understand", but "understand"
  needs sometimes to instantiate evars to ensure the type of an evar
  is not its original type but the type of its instance (what can
  e.g. lower a universe level); we would need here to update evars
  type at the same time we define them but this would need in turn to
  check the convertibility of the actual and expected type since otherwise
  type-checking constraints may disappear;
- typing pattern is apparently expensive in time; is it worth to do it
  for the benefit of pattern-matching compilation and coercion insertion?

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

19 files changed, 146 insertions, 97 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e594f9a9df..155fd1c026 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -381,7 +381,7 @@ let rec subst_aconstr subst bound raw =
 	  AHole (Evd.InternalHole)
   | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
     | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
-    | Evd.ImpossibleCase) -> raw
+    | Evd.ImpossibleCase | Evd.MatchingVar _) -> raw
 
   | ACast (r1,k) ->
       match k with
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fe7038d3a3..ad6e2c61bb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -1043,7 +1043,7 @@ let rec glob_printers =
     (pr_glob_tactic_level,
      (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
      (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
-     (fun c -> pr_lconstr_pattern_env (Global.env()) c),
+     (fun (_,c) -> pr_lconstr_pattern_env (Global.env()) c),
      (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
      (fun env -> pr_or_var (pr_inductive env)),
      pr_ltac_or_var (pr_located pr_ltac_constant),
@@ -1083,7 +1083,8 @@ let _ = Tactic_debug.set_match_pattern_printer
 
 let _ = Tactic_debug.set_match_rule_printer
   (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)
+    pr_match_rule false (pr_glob_tactic (Global.env())) 
+      (fun (_,p) -> pr_constr_pattern p) rl)
 
 open Extrawit
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 16cc3a7316..e1a16ce498 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -215,9 +215,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (array_last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pattern_of_constr f, Array.map aux args)
+          PApp (pattern_of_constr Evd.empty f, Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr c
+      | _ -> pattern_of_constr Evd.empty c
   in
   aux bodyi
 
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 7d1f2cd62e..f909f9e0a9 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -569,7 +569,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
 
-  let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+  let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -581,7 +581,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
-    let c = nf_evar !evdref c' in
+    let c = if expand_evar then nf_evar !evdref c' else c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
 
@@ -606,30 +606,30 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
-  let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+  let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
   let understand_gen kind sigma env c =
-    snd (ise_pretype_gen true true sigma env ([],[]) kind c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
 
   let understand sigma env ?expected_type:exptyp c =
-    snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
 
   let understand_type sigma env c =
-    snd (ise_pretype_gen false true sigma env ([],[]) IsType c)
+    snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
 
-  let understand_ltac sigma env lvar kind c =
-    ise_pretype_gen false true sigma env lvar kind c
+  let understand_ltac expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false true sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-    ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
   let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-    pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
 end
 
 module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 476724ba6d..32a1755ca0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -189,6 +189,7 @@ let string_of_hole_kind = function
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
   | GoalEvar -> "GoalEvar"
   | ImpossibleCase -> "ImpossibleCase"
+  | MatchingVar _ -> "MatchingVar"
 
 let evars_of_term evc init c =
   let rec evrec acc c =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0d9a51ba37..ccba1d2cc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -32,6 +32,7 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
+  | MatchingVar of bool * identifier
 
 (* The type of mappings for existential variables *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3974e65b42..b82e6d998d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -94,6 +94,7 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
+  | MatchingVar of bool * identifier
 
 (*********************************************************************)
 (*** Existential variables and unification states ***)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 9acdd15855..7b8c623607 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -89,7 +89,10 @@ let head_of_constr_reference c = match kind_of_term c with
   | Var id -> VarRef id
   | _ -> anomaly "Not a rigid reference"
 
-let rec pattern_of_constr t =
+open Evd
+
+let pattern_of_constr sigma t =
+  let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
@@ -100,11 +103,25 @@ let rec pattern_of_constr t =
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
-    | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
+    | App (f,a) ->
+        (match 
+          match kind_of_term f with
+            Evar (evk,args) ->
+              (match snd (Evd.evar_source evk sigma) with
+                  MatchingVar (true,n) -> Some n
+                | _ -> None)
+            | _ -> None
+          with
+            | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a))
+            | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a))
     | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind sp        -> PRef (canonical_gr (IndRef sp))
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
-    | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
+    | Evar (evk,ctxt) ->
+        (match snd (Evd.evar_source evk sigma) with
+          | MatchingVar (b,n) -> assert (not b); PMeta (Some n)
+          | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | _ -> PMeta None)
     | Case (ci,p,a,br) ->
 	let cip = ci.ci_pp_info in
 	let no = Some (ci.ci_npar,cip.ind_nargs) in
@@ -113,6 +130,7 @@ let rec pattern_of_constr t =
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
     | CoFix f -> PCoFix f
+  in pattern_of_constr t
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -144,11 +162,12 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern subst pat = match pat with
+let rec subst_pattern subst pat =
+  match pat with
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr t
+	 pattern_of_constr Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index b0229ab618..0e87025fc8 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : constr -> constr_pattern
+val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern
 
 (* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 288eb9da22..cfe028aa51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -108,15 +108,16 @@ sig
   (* Generic call to the interpreter from rawconstr to constr, failing
      unresolved holes in the rawterm cannot be instantiated.
 
-     In [understand_ltac sigma env ltac_env constraint c],
+     In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
+     expand_evars : expand inferred evars by their value if any
      sigma : initial set of existential variables (typically dependent subgoals)
      ltac_env : partial substitution of variables (used for the tactic language)
      constraint : tell if interpreted as a possibly constrained term or a type
   *)
 
   val understand_ltac :
-    evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -156,7 +157,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_map ref -> env ->
+    bool -> bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
@@ -307,7 +308,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | RPatVar (loc,(someta,n)) ->
-	anomaly "Found a pattern variable in a rawterm to type"
+	let ty =
+          match tycon with
+            | Some (None, ty) -> ty
+            | None | Some _ ->
+		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+        let k = MatchingVar (someta,n) in
+	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | RHole (loc,k) ->
 	let ty =
@@ -418,7 +425,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	          let sigma =  !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
-		  make_judge c t
+		  make_judge c (* use this for keeping evars: resj.uj_val *) t
               | _ -> resj end
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -661,7 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env !evdref tj.utj_val v
 
-  let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+  let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -673,7 +680,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
-    let c = nf_evar !evdref c' in
+    let c = if expand_evar then nf_evar !evdref c' else c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
 
@@ -701,30 +708,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
-  let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+  let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
   let understand_gen kind sigma env c =
-    snd (ise_pretype_gen true true sigma env ([],[]) kind c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
 
   let understand sigma env ?expected_type:exptyp c =
-    snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
 
   let understand_type sigma env c =
-    snd (ise_pretype_gen true true sigma env ([],[]) IsType c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
 
-  let understand_ltac sigma env lvar kind c =
-    ise_pretype_gen false false sigma env lvar kind c
+  let understand_ltac expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false false sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-    ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
   let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-    pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
 end
 
 module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e3b18f73cb..75bd7874e7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -51,15 +51,16 @@ sig
   (* Generic call to the interpreter from rawconstr to constr, failing
      unresolved holes in the rawterm cannot be instantiated.
 
-     In [understand_ltac sigma env ltac_env constraint c],
+     In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
+     expand_evars : expand inferred evars by their value if any
      sigma : initial set of existential variables (typically dependent subgoals)
      ltac_env : partial substitution of variables (used for the tactic language)
      constraint : tell if interpreted as a possibly constrained term or a type
   *)
 
   val understand_ltac :
-    evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -97,7 +98,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_map ref -> env ->
+    bool -> bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b3976704af..e4fab3f2f8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     error "Instantiate called on already-defined evar";
   let env = Evd.evar_env evi in
   let sigma',typed_c =
-    try Pretyping.Default.understand_ltac sigma env ltac_var
+    try Pretyping.Default.understand_ltac true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1d4766494d..04b7a225c7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -273,7 +273,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
 (* Globalized tactics *)
 and glob_tactic_expr =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -317,7 +317,7 @@ type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
 
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -327,7 +327,7 @@ type glob_atomic_tactic_expr =
 
 type glob_tactic_arg =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index ab59f208af..0a5e6087b1 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -24,7 +24,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
 val set_match_pattern_printer :
   (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
 val set_match_rule_printer :
-  ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+  ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
     unit
 
 (* Debug information *)
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
 
 (* Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 59791f011d..0e4091b3cb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -268,12 +268,12 @@ let dummy_goal =
   {it = make_evar empty_named_context_val mkProp;
    sigma = empty}
 
-let make_exact_entry pri (c,cty) =
+let make_exact_entry sigma pri (c,cty) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Pattern.pattern_of_constr cty in
+	let pat = Pattern.pattern_of_constr sigma cty in
 	let head = 
 	  try head_of_constr_reference (fst (head_constr cty)) 
 	  with _ -> failwith "make_exact_entry" 
@@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Pattern.pattern_of_constr c' in
+	let pat = Pattern.pattern_of_constr sigma c' in
         let hd = (try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = List.length (clenv_missing ce) in
@@ -317,7 +317,7 @@ let make_resolves env sigma flags pri c =
   let ents =
     map_succeed
       (fun f -> f (c,cty))
-      [make_exact_entry pri; make_apply_entry env sigma flags pri]
+      [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
   in
   if ents = [] then
     errorlabstrm "Hint"
@@ -354,7 +354,7 @@ let make_trivial env sigma c =
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
-         pat = Some (Pattern.pattern_of_constr (clenv_type ce));
+         pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce));
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
@@ -1102,7 +1102,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) =
   let ents =
     map_succeed
       (fun f -> f (mkVar id,ty))
-      [make_exact_entry None; make_apply_entry env sigma (true,true,false) None]
+      [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None]
   in
   ents
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index fe59dc1e12..072e02989a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -112,7 +112,7 @@ val print_hint_db : Hint_db.t -> unit
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
-val make_exact_entry : int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
 
 (* [make_apply_entry (eapply,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6f928e0966..b77425f0d6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -271,7 +271,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
     if keep then let c = mkVar id in
       map_succeed 
 	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
-	[make_exact_entry pri; make_apply_entry env sigma flags pri]
+	[make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
     else []
 
 let pf_filtered_hyps gls = 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bef5563454..f031df2560 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -497,15 +497,15 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let c' =
-    warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c
+    warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
   in
   (c',if !strict_check then None else Some c)
 
-let intern_constr = intern_constr_gen false
-let intern_type = intern_constr_gen true
+let intern_constr = intern_constr_gen false false
+let intern_type = intern_constr_gen false true
 
 (* Globalize bindings *)
 let intern_binding ist (loc,b,c) =
@@ -604,15 +604,17 @@ let intern_hyp_location ist (((b,occs),id),hl) =
   (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
 
 (* Reads a pattern *)
-let intern_pattern sigma env ?(as_type=false) lfun = function
+let intern_pattern ist ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in
-      ido, metas, Subterm (b,ido,pat)
+      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+      let c = intern_constr_gen true false ist pc in
+      ido, metas, Subterm (b,ido,(c,pat))
   | Term pc ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in
-      None, metas, Term pat
+      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in
+      let c = intern_constr_gen true false ist pc in
+      None, metas, Term (c,pat)
 
 let intern_constr_may_eval ist = function
   | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
@@ -649,16 +651,16 @@ let extend_values_with_bindings (ln,lm) lfun =
   lmatch@lfun@lnames
 
 (* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps sigma env lfun = function
+let rec intern_match_goal_hyps ist lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
-      let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
-      let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in
+      let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
+      let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
       let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
   | (Def ((_,na) as locna,mv,mp))::tl ->
-      let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
-      let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
-      let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in
+      let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
+      let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
+      let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
       let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
       lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
@@ -714,7 +716,7 @@ let rec intern_atomic lf ist x =
   | TacAssert (otac,ipat,c) ->
       TacAssert (Option.map (intern_tactic ist) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
-                 intern_constr_gen (otac<>None) ist c)
+                 intern_constr_gen false (otac<>None) ist c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (fun (c,na) ->
 	               intern_constr_with_occurrences ist c,
@@ -904,8 +906,8 @@ and intern_match_rule ist = function
       All (intern_tactic ist tc) :: (intern_match_rule ist tl)
   | (Pat (rl,mp,tc))::tl ->
       let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
-      let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in
-      let ido,metas2,pat = intern_pattern sigma env lfun mp in
+      let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+      let ido,metas2,pat = intern_pattern ist lfun mp in
       let metas = list_uniquize (metas1@metas2) in
       let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
       Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
@@ -1312,7 +1314,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   (* Side-effect *)
   !evdref,c
 
-let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars),typs =
     extract_ltac_vars_data ist sigma env in
   let c = match ce with
@@ -1325,25 +1327,34 @@ let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
       intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
   let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
   let evd,c =
-    catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c in
-  let evd,c = solve_remaining_evars fail_evar use_classes env sigma evd c in
+    catch_error trace
+      (understand_ltac expand_evar sigma env (typs,unbndltacvars) kind) c in
+  let evd,c =
+    if expand_evar then
+      solve_remaining_evars fail_evar use_classes env sigma evd c
+    else
+      evd,c in
   db_constr ist.debug env c;
   (evd,c)
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  snd (interp_gen kind ist true true env sigma c)
+  snd (interp_gen kind ist true true true env sigma c)
 
 let interp_constr = interp_constr_gen (OfType None)
 
 let interp_type = interp_constr_gen IsType
 
 (* Interprets an open constr *)
-let interp_open_constr_gen kind ist = interp_gen kind ist false false
+let interp_open_constr_gen kind ist = interp_gen kind ist true false false
 
 let interp_open_constr ccl =
   interp_open_constr_gen (OfType ccl)
 
+let interp_typed_pattern ist env sigma c =
+  let sigma, c = interp_gen (OfType None) ist false false false env sigma c in
+  pattern_of_constr sigma c
+
 (* Interprets a constr expression casted by the current goal *)
 let pf_interp_casted_constr ist gl c =
   interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c
@@ -1626,13 +1637,18 @@ let give_context ctxt = function
   | Some id -> [id,VConstr_context ctxt]
 
 (* Reads a pattern by substituting vars of lfun *)
-let eval_pattern lfun c =
-  let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr c))) lfun in
-  instantiate_pattern lvar c
+let use_types = false
+
+let eval_pattern lfun ist env sigma (c,pat) =
+  if use_types then
+    interp_typed_pattern ist env sigma c
+  else
+    let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr Evd.empty c))) lfun in
+    instantiate_pattern lvar pat
 
-let read_pattern lfun = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
-  | Term pc -> Term (eval_pattern lfun pc)
+let read_pattern lfun ist env sigma = function
+  | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+  | Term c -> Term (eval_pattern lfun ist env sigma c)
 
 (* Reads the hypotheses of a Match Context rule *)
 let cons_and_check_name id l =
@@ -1642,23 +1658,23 @@ let cons_and_check_name id l =
       " used twice in the same pattern."))
   else id::l
 
-let rec read_match_goal_hyps lfun lidh = function
+let rec read_match_goal_hyps lfun ist env sigma lidh = function
   | (Hyp ((loc,na) as locna,mp))::tl ->
       let lidh' = name_fold cons_and_check_name na lidh in
-      Hyp (locna,read_pattern lfun mp)::
-	(read_match_goal_hyps lfun lidh' tl)
+      Hyp (locna,read_pattern lfun ist env sigma mp)::
+	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | (Def ((loc,na) as locna,mv,mp))::tl ->
       let lidh' = name_fold cons_and_check_name na lidh in
-      Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
-	(read_match_goal_hyps lfun lidh' tl)
+      Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
+	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | [] -> []
 
 (* Reads the rules of a Match Context or a Match *)
-let rec read_match_rule lfun = function
-  | (All tc)::tl -> (All tc)::(read_match_rule lfun tl)
+let rec read_match_rule lfun ist env sigma = function
+  | (All tc)::tl -> (All tc)::(read_match_rule lfun ist env sigma tl)
   | (Pat (rl,mp,tc))::tl ->
-      Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc)
-      :: read_match_rule lfun tl
+      Pat (read_match_goal_hyps lfun ist env sigma [] rl, read_pattern lfun ist env sigma mp,tc)
+      :: read_match_rule lfun ist env sigma tl
   | [] -> []
 
 (* For Match Context and Match *)
@@ -1989,7 +2005,7 @@ and interp_match_goal ist goal lz lr lmr =
 		       else mt()) ++ str"."))
     end in
     apply_match_goal ist env goal 0 lmr
-      (read_match_rule (fst (constr_list ist env)) lmr)
+      (read_match_rule (fst (constr_list ist env)) ist env (project goal) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -2158,7 +2174,7 @@ and interp_match ist g lz constr lmr =
         debugging_exception_step ist true e
           (fun () -> str "evaluation of the matched expression");
         raise e in
-  let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
+  let ilr = read_match_rule (fst (constr_list ist (pf_env g))) ist (pf_env g) (project g) lmr in
   let res =
      try apply_match ist csr ilr with e ->
        debugging_exception_step ist true e (fun () -> str "match expression");
@@ -2589,8 +2605,8 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
-  | Term pc -> Term (subst_pattern subst pc)
+  | Subterm (b,ido,(c,pc)) -> Subterm (b,ido,(subst_rawconstr subst c,subst_pattern subst pc))
+  | Term (c,pc) -> Term (subst_rawconstr subst c,subst_pattern subst pc)
 
 let rec subst_match_goal_hyps subst = function
   | Hyp (locs,mp) :: tl ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 852e7588af..fdd05b870f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -350,6 +350,8 @@ let explain_hole_kind env evi = function
       str "an existential variable"
   | ImpossibleCase ->
       str "the type of an impossible pattern-matching clause"
+  | MatchingVar _ ->
+      assert false
 
 let explain_not_clean env ev t k =
   let env = make_all_name_different env in