- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec

  "pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1


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

14 files changed, 121 insertions, 103 deletions

diff --git a/CHANGES b/CHANGES
index bf11db4680..9bd471ec03 100644
--- a/CHANGES
+++ b/CHANGES
@@ -161,8 +161,8 @@ Tactics
 - Tactic "apply" now able to reason modulo unfolding of constants
   (possible source of incompatibility in situations where apply may fail, 
   e.g. as argument of a try or a repeat and in a ltac function);
-  version of apply that does not unfold is renamed into "simple apply"
-  (usable for compatibility or for automation).
+- The version of apply that does not unfold, nor use types in "with" bindings
+  is renamed into "simple apply" (usable for compatibility or for automation).
 - Tactic "apply" now able to traverse conjunctions and to select the first 
   matching lemma among the components of the conjunction; tactic apply also
   able to apply lemmas of conclusion an empty type.
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 9eac4fbaed..2569404b0d 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -314,7 +314,7 @@ module Coercion = struct
   let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, Option.map (app_opt coercion) v, t
+      !evars, Option.map (app_opt coercion) v
 	
   (* Taken from pretyping/coercion.ml *)
 
@@ -416,11 +416,15 @@ module Coercion = struct
 		 uj_type = typ' }
 
 
-  let inh_coerce_to_fail env isevars c1 v t =
+  let inh_coerce_to_fail env evd rigidonly v t c1 =
+    if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
+    then
+      raise NoCoercion
+    else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env (evars_of isevars) c1 in
-	let t2,i2 = class_of1 env (evars_of isevars) t in
+	let t1,i1 = class_of1 env (evars_of evd) c1 in
+	let t2,i2 = class_of1 env (evars_of evd) t in
 	let p = lookup_path_between (i2,i1) in
 	  match v with
 	      Some v -> 
@@ -429,102 +433,73 @@ module Coercion = struct
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
     in
-      try (the_conv_x_leq env t' c1 isevars, v', t')
+      try (the_conv_x_leq env t' c1 evd, v')
       with Reduction.NotConvertible -> raise NoCoercion
 
-  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+
+  let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
 (*     (try *)
 (*        debug 1 (str "inh_conv_coerce_to_fail called for " ++ *)
 (* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
 (* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
-(* 	      Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* 	      Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *)
 (* 	      Termops.print_env env); *)
 (*      with _ -> ()); *)
-    try (the_conv_x_leq env t c1 isevars, v, t)
+    try (the_conv_x_leq env t c1 evd, v)
     with Reduction.NotConvertible ->
-      (try 
-	 inh_coerce_to_fail env isevars c1 v t
-	 with NoCoercion ->
-	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = Option.map (whd_betadeltaiota env (evars_of isevars)) v in
-		    let (evd',b) =
-		      match v' with 
-			  Some v' ->
-			    (match kind_of_term v' with
-			       | Lambda (x,v1,v2) ->
-				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
-				    with Reduction.NotConvertible -> (isevars, None))
-			       | _  -> (isevars, None))
-			| None -> (isevars, None)
-		    in 
-		      (match b with
-			   Some (x, v1, v2) ->
-			     let env1 = push_rel (x,None,v1) env in
-			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
-						       (Some v2) t2 u2 in
-			       (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', 
-				mkProd (x, v1, t2'))
-			 | None ->
-			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-			     (* has type (name:u1)u2 (with v' recursively obtained) *)
-			     let name = (match name with 
-					   | Anonymous -> Name (id_of_string "x")
-					   | _ -> name) in
-			     let env1 = push_rel (name,None,u1) env in
-			     let (evd', v1', t1') =
-			       inh_conv_coerce_to_fail loc env1 isevars
-				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
-			     in
-			     let (evd'', v2', t2') = 
-			       let v2 =
-				 match v with 
-				     Some v -> Option.map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
-				   | None -> None
-			       and evd', t2 =
-				 match v1' with 
-				     Some v1' -> evd', subst1 v1' t2
-				   | None -> 
-				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
-					 evd', subst1 ev t2
-			       in
-				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
-			     in
-			       (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2',
-				mkProd (name, u1, t2')))
-		| _ -> raise NoCoercion))
+    try inh_coerce_to_fail env evd rigidonly v t c1
+    with NoCoercion ->
+    match
+      kind_of_term (whd_betadeltaiota env (evars_of evd) t),
+      kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
+    with
+    | Prod (name,t1,t2), Prod (_,u1,u2) -> 
+        (* Conversion did not work, we may succeed with a coercion. *)
+        (* We eta-expand (hence possibly modifying the original term!) *)
+	(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
+	(* has type forall (x:u1), u2 (with v' recursively obtained) *)
+	let name = match name with 
+	  | Anonymous -> Name (id_of_string "x")
+	  | _ -> name in
+	let env1 = push_rel (name,None,u1) env in
+	let (evd', v1) =
+	  inh_conv_coerce_to_fail loc env1 evd rigidonly
+            (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
+        let v1 = Option.get v1 in
+	let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
+        let t2 = Termops.subst_term v1 t2 in
+	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
+	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
+    | _ -> raise NoCoercion
 
-	
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) =
+  let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
 (*     (try *)
 (*        trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *)
 (* 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *)
 (* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
-(* 	      Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* 	      Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *)
 (* 	      Termops.print_env env); *)
 (*      with _ -> ()); *)
     match n with
 	None ->
-	  let (evd', val', type') = 
+	  let (evd', val') = 
 	    try 
-	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
-	      let sigma = evars_of isevars in
+	      let sigma = evars_of evd in
 		try
-		  coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+		  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 		with NoSubtacCoercion ->
 		  error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
 	    (evd',{ uj_val = val'; uj_type = t })
       | Some (init, cur) ->
-	  (isevars, cj)
+	  (evd, cj)
 
-  let inh_conv_coerce_rigid_to _ _ _ _ _ =
-    failwith "inh_conv_coerce_rigid_to: TODO"
+  let inh_conv_coerce_to = inh_conv_coerce_to_gen false
+  let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
 (*     (try *)
@@ -550,7 +525,7 @@ module Coercion = struct
 	      env', rng, lift nabs t'
 	  in
 	    try
-	      pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+	      fst (try inh_conv_coerce_to_fail loc env' isevars false None t t'
 		   with NoCoercion ->
 		     coerce_itf loc env' isevars None t t')
 	    with NoSubtacCoercion ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a76b2386cf..3153d45566 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -72,6 +72,22 @@ let lpar_id_colon =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+(* idem for (x1..xn:t) [not efficient but exceptional use] *)
+let check_lpar_ids_colon =
+  Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("","(")] ->
+	    let rec aux tok n =
+              match tok with
+              | ("IDENT",id) ->
+                  (match list_last (Stream.npeek n strm) with
+                    | ("", ":") -> ()
+                    | tok -> aux tok (n+1))
+              | _ -> raise Stream.Failure
+	    in aux (list_last (Stream.npeek 2 strm)) 3
+        | _ -> raise Stream.Failure)
+
 let guess_lpar_ipat s strm =
   match Stream.npeek 1 strm with
     | [("","(")] ->
@@ -343,7 +359,8 @@ GEXTEND Gram
   ;
   simple_named_binder:
     [ [ id=identref -> ([id],CHole (loc, None))
-      | "("; idl=LIST1 identref; ":"; c=lconstr; ")" -> (idl,c) 
+      | check_lpar_ids_colon; 
+        "("; idl=LIST1 identref; ":"; c=lconstr; ")" -> (idl,c) 
     ] ]
   ;
   fixdecl:
@@ -367,7 +384,7 @@ GEXTEND Gram
 	  let first_args = appl_args_of_simple_named_binders bl in
 	  (Names.Anonymous, CApp(loc,(None,CRef (Ident lid)),first_args@args))
       | "("; c = lconstr; ")" -> (Names.Anonymous, c) 
-      | c = lconstr -> (Names.Anonymous, c) ] ]
+      | c = constr -> (Names.Anonymous, c) ] ]
   ;
   hintbases:
     [ [ "with"; "*" -> None
@@ -457,8 +474,14 @@ GEXTEND Gram
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
 	  TacMutualCofix (false,id,List.map mk_cofix_tac fd)
 
+(*
       | IDENT "pose"; (na,c) = constr_or_decl ->
 	  TacLetTac (na,c,nowhere)
+*)
+      | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
+	  TacLetTac (Names.Name id,b,nowhere)
+      | IDENT "pose"; b = constr ->
+	  TacLetTac (Names.Anonymous,b,nowhere)
       | IDENT "set"; (na,c) = constr_or_decl; p = clause ->
 	  TacLetTac (na,c,p)
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index e7423c748b..4d0318ba2f 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -402,15 +402,17 @@ let clenv_unify_binding_type clenv c t u =
     with e when precatchable_exception e ->
       TypeNotProcessed, clenv, c
 
-let clenv_assign_binding clenv k (sigma,c) =
+let clenv_assign_binding use_types clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
   let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
   let c_typ = clenv_hnf_constr clenv' c_typ in
-  let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
+  let status,clenv'',c = 
+    if use_types then clenv_unify_binding_type clenv' c c_typ k_typ
+    else TypeNotProcessed, clenv, c in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
-let clenv_match_args bl clenv =
+let clenv_match_args use_types bl clenv =
   if bl = [] then
     clenv
   else
@@ -423,7 +425,7 @@ let clenv_match_args bl clenv =
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding clenv k sc)
+	  clenv_assign_binding use_types clenv k sc)
       clenv bl
 
 let clenv_constrain_last_binding c clenv =
@@ -431,15 +433,15 @@ let clenv_constrain_last_binding c clenv =
   let k =
     try list_last all_mvs 
     with Failure _ -> error "clenv_constrain_with_bindings" in
-  clenv_assign_binding clenv k (Evd.empty,c)
+  clenv_assign_binding true clenv k (Evd.empty,c)
 
-let clenv_constrain_dep_args hyps_only bl clenv =
+let clenv_constrain_dep_args use_types hyps_only bl clenv =
   if bl = [] then
     clenv
   else
     let occlist = clenv_dependent hyps_only clenv in
     if List.length occlist = List.length bl then
-      List.fold_left2 clenv_assign_binding clenv occlist bl
+      List.fold_left2 (clenv_assign_binding use_types) clenv occlist bl
     else 
       error ("Not the right number of missing arguments (expected "
 	     ^(string_of_int (List.length occlist))^")")
@@ -447,18 +449,18 @@ let clenv_constrain_dep_args hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
+let make_clenv_binding_gen use_types hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args hyps_only largs clause
+      clenv_constrain_dep_args use_types hyps_only largs clause
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
+      clenv_match_args use_types lbind clause
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
+let make_clenv_binding_apply use_types = make_clenv_binding_gen use_types true 
+let make_clenv_binding = make_clenv_binding_gen true false None
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index dfa7513495..954e5607f1 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -97,7 +97,8 @@ val clenv_missing : clausenv -> metavariable list
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
 (* defines metas corresponding to the name of the bindings *)
-val clenv_match_args : arg_bindings -> clausenv -> clausenv
+val clenv_match_args : bool (* unify types *) -> arg_bindings -> clausenv -> 
+  clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
@@ -106,9 +107,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 (* the arity of the lemma is fixed *)
 (* the optional int tells how many prods of the lemma have to be used *)
 (* use all of them if None *)
+(* boolean tells to unify immediately unifiable types of the bindings *)
 val make_clenv_binding_apply :
-  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
-   clausenv
+  bool -> int option -> evar_info sigma -> constr * constr -> 
+    open_constr bindings -> clausenv
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bd023721ae..5a99adb5a6 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -160,7 +160,7 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
-  let inh_coerce_to_fail env evd rigidonly v c1 t =
+  let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
       raise NoCoercion
@@ -183,7 +183,7 @@ module Default = struct
   let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try (the_conv_x_leq env t c1 evd, v)
     with Reduction.NotConvertible ->
-    try inh_coerce_to_fail env evd rigidonly v c1 t
+    try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
       kind_of_term (whd_betadeltaiota env (evars_of evd) t),
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b140ad51aa..90d6bb081b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,18 +120,21 @@ let sort_eqns = unify_r2l
 type unify_flags = { 
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
+  use_types : bool;
   modulo_delta : Names.transparent_state;
 }
 
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = full_transparent_state;
 }
 
-let default_no_delta_unify_flags = {
+let simple_apply_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly = false;
+  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
@@ -723,5 +726,6 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 		    error "Cannot solve a second-order unification problem")
 	    
       (* General case: try first order *)
-      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
-
+      | _ ->
+	  if flags.use_types then w_typed_unify env cv_pb flags ty1 ty2 evd
+	  else w_unify_0 env cv_pb flags ty1 ty2 evd
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 1b8f9ccd8b..8cfa209480 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,11 +17,12 @@ open Evd
 type unify_flags = { 
   modulo_conv_on_closed_terms : Names.transparent_state option; 
   use_metas_eagerly : bool;
+  use_types : bool;
   modulo_delta : Names.transparent_state;
 }
 
 val default_unify_flags : unify_flags
-val default_no_delta_unify_flags : unify_flags
+val simple_apply_unify_flags : unify_flags
 
 (* The "unique" unification fonction *)
 val w_unify :
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 22dcca2890..babf53c9fb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -98,6 +98,7 @@ open Unification
 let fail_quick_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
+  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 66fde8f6bf..8823efe0bd 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -586,6 +586,7 @@ open Unification
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
+  use_types = false;
   modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4319a1d3de..72bc85c2f4 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -72,6 +72,7 @@ open Unification
 let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = var_full_transparent_state;
 }
 
@@ -631,6 +632,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
+  Unification.use_types = true;
   Unification.modulo_delta = empty_transparent_state;
 }
 
@@ -639,6 +641,7 @@ let conv_transparent_state = (Idpred.empty, Cpred.full)
 let rewrite2_unif_flags = {
   Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
   Unification.use_metas_eagerly = true;
+  Unification.use_types = true;
   Unification.modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index dc8ff2b9cd..b5710c9666 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,12 +1734,14 @@ let check_evar_map_of_evars_defs evd =
 let rewrite_unif_flags = {
   modulo_conv_on_closed_terms = None;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
 let rewrite2_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dd8aa12941..1bd65ecdf6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -329,7 +329,7 @@ let general_elim_then_using mk_elim
   ind indclause gl =
   let elim = mk_elim ind gl in
   (* applying elimination_scheme just a little modified *)
-  let indclause' = clenv_match_args indbindings indclause in
+  let indclause' = clenv_match_args true indbindings indclause in
   let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
@@ -350,7 +350,7 @@ let general_elim_then_using mk_elim
 	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
-  let elimclause' = clenv_match_args elimbindings elimclause' in
+  let elimclause' = clenv_match_args true elimbindings elimclause' in
   let branchsigns = compute_construtor_signatures isrec ind in
   let brnames = compute_induction_names (Array.length branchsigns) allnames in
   let after_tac ce i gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d3f7cc5f15..cd8ad4c14d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -551,6 +551,7 @@ let last_arg c = match kind_of_term c with
 let elim_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = true;
+  use_types = true;
   modulo_delta = empty_transparent_state;
 }
 
@@ -672,9 +673,10 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let general_apply with_delta with_destruct with_evars (c,lbind) gl =
+let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if with_delta then default_unify_flags else default_no_delta_unify_flags in
+    if with_delta_and_types then default_unify_flags
+    else simple_apply_unify_flags in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
@@ -684,7 +686,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let try_apply thm_ty nprod =
     let n = nb_prod thm_ty - nprod in
     if n<0 then error "Apply: theorem has not enough premisses.";
-    let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+    let clause =
+     make_clenv_binding_apply with_delta_and_types (Some n) gl (c,thm_ty) lbind
+    in
     Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
   try try_apply thm_ty0 concl_nprod
   with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->