- Backtrack sur option with_types suite à confusion sur l'utilisation

  des types des with-bindings dans la 8.1 [ceux-ci étaient déjà
  utilisés et ce qui est vraiment nouveau est que l'unification est
  maintenant celle de evarconv alors que c'était avant un mélange
  d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je
  renonce à maintenir la compatibilité (on se retrouve donc avec un
  exemple qui fonctionne différement dans TermsConv.v de CoLoR).
- Robustesse accrue pour la nouvelle facilité de syntaxe de binding
  avec paramètre pour pose/set.



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

12 files changed, 58 insertions, 110 deletions

diff --git a/CHANGES b/CHANGES
index 9bd471ec0..bf11db468 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);
-- 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).
+  version of apply that does not unfold 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/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3153d4556..7803cd076 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -17,7 +17,6 @@ open Tacexpr
 open Rawterm
 open Genarg
 open Topconstr
-open Term
 open Libnames
 
 let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
@@ -72,21 +71,29 @@ 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 =
+(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
+let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
+      let rec skip_to_rpar n =
+	match list_last (Stream.npeek n strm) with
+        | ("",")") -> n+1
+	| ("",".") -> raise Stream.Failure
+	| _ -> skip_to_rpar (n+1) in
+      let rec skip_names n =
+	match list_last (Stream.npeek n strm) with
+        | ("IDENT",_) | ("","_") -> skip_names (n+1)
+	| ("",":") -> skip_to_rpar (n+1) (* skip a constr *)
+	| _ -> raise Stream.Failure in
+      let rec skip_binders n =
+	match list_last (Stream.npeek n strm) with
+        | ("","(") -> skip_binders (skip_names (n+1))
+        | ("IDENT",_) | ("","_") -> skip_binders (n+1)
+	| ("",":=") -> ()
+	| _ -> raise Stream.Failure in
       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)
+      | [("","(")] -> skip_binders 2
+      | _ -> raise Stream.Failure)
 
 let guess_lpar_ipat s strm =
   match Stream.npeek 1 strm with
@@ -106,13 +113,6 @@ let guess_lpar_coloneq =
 let guess_lpar_colon =
   Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":")
 
-let test_not_ident =
-  Gram.Entry.of_parser "not_ident"
-    (fun strm ->
-      match Stream.npeek 1 strm with
-        | [("IDENT",_)] -> raise Stream.Failure
-	| _ -> ())
-
 open Constr
 open Prim
 open Tactic
@@ -142,18 +142,6 @@ let induction_arg_of_constr (c,lbind as clbind) =
     with _ -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
-(* Turn a simple binder as the argument for an application *)
-let appl_args_of_simple_named_binder = function
-| (idl,CHole _) ->
-    List.map (fun id -> CRef (Ident id), None) idl
-| (idl,t) -> 
-    let loc = join_loc (fst (List.hd idl)) (constr_loc t) in
-    let mk id = CCast (loc,CRef (Ident id),CastConv (DEFAULTcast,t)), None in
-    List.map mk idl
-
-let appl_args_of_simple_named_binders bl =
-  List.flatten (List.map appl_args_of_simple_named_binder bl)
-
 let rec mkCLambdaN_simple_loc loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll -> 
@@ -161,12 +149,7 @@ let rec mkCLambdaN_simple_loc loc bll c =
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
   | [] -> c
 
-let mkCLambdaN_simple bl1 bl2 c =
-  let bl =
-    List.map (fun (idl,c) ->
-      (List.map (fun (loc,id) -> (loc,Names.Name id)) idl,
-       Default Explicit,c)) bl1
-      @ bl2 in
+let mkCLambdaN_simple bl c =
   if bl=[] then c
   else
     let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in
@@ -353,14 +336,8 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
-    ] ]
-  ;
-  simple_named_binder:
-    [ [ id=identref -> ([id],CHole (loc, None))
-      | check_lpar_ids_colon; 
-        "("; idl=LIST1 identref; ":"; c=lconstr; ")" -> (idl,c) 
+    [ [ na=name -> ([na],Default Explicit,CHole (loc, None))
+      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) 
     ] ]
   ;
   fixdecl:
@@ -375,16 +352,9 @@ GEXTEND Gram
     [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
         (loc,id,bl,None,ty) ] ]
   ;
-  constr_or_decl:
-    [ [ "("; lid = identref; bl1 = LIST0 simple_named_binder; 
-        ":="; c = lconstr; ")" ->
-          (Names.Name (snd lid), mkCLambdaN_simple bl1 [] c)
-      | "("; lid = identref; bl = LIST0 simple_named_binder; 
-	 args = LIST0 appl_arg; ")" ->
-	  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 = constr -> (Names.Anonymous, c) ] ]
+  bindings_with_parameters:
+    [ [ check_for_coloneq; "(";  id = ident; bl = LIST0 simple_binder; 
+        ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
   ;
   hintbases:
     [ [ "with"; "*" -> None
@@ -474,16 +444,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; ")" ->
+      | IDENT "pose"; (id,b) = bindings_with_parameters ->
 	  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)
+      | IDENT "set"; (id,c) = bindings_with_parameters; p = clause ->
+	  TacLetTac (Names.Name id,c,p)
+      | IDENT "set"; c = constr; p = clause ->
+          TacLetTac (Names.Anonymous,c,p)
 
       (* Begin compatibility *)
       | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 4d0318ba2..e7423c748 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -402,17 +402,15 @@ let clenv_unify_binding_type clenv c t u =
     with e when precatchable_exception e ->
       TypeNotProcessed, clenv, c
 
-let clenv_assign_binding use_types clenv k (sigma,c) =
+let clenv_assign_binding 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 = 
-    if use_types then clenv_unify_binding_type clenv' c c_typ k_typ
-    else TypeNotProcessed, clenv, c in
+  let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
-let clenv_match_args use_types bl clenv =
+let clenv_match_args bl clenv =
   if bl = [] then
     clenv
   else
@@ -425,7 +423,7 @@ let clenv_match_args use_types bl clenv =
           if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding use_types clenv k sc)
+	  clenv_assign_binding clenv k sc)
       clenv bl
 
 let clenv_constrain_last_binding c clenv =
@@ -433,15 +431,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 true clenv k (Evd.empty,c)
+  clenv_assign_binding clenv k (Evd.empty,c)
 
-let clenv_constrain_dep_args use_types hyps_only bl clenv =
+let clenv_constrain_dep_args 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 use_types) clenv occlist bl
+      List.fold_left2 clenv_assign_binding clenv occlist bl
     else 
       error ("Not the right number of missing arguments (expected "
 	     ^(string_of_int (List.length occlist))^")")
@@ -449,18 +447,18 @@ let clenv_constrain_dep_args use_types hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen use_types hyps_only n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args use_types hyps_only largs clause
+      clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args use_types lbind clause
+      clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-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
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
+let make_clenv_binding = make_clenv_binding_gen false None
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 954e5607f..dfa751349 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -97,8 +97,7 @@ 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 : bool (* unify types *) -> arg_bindings -> clausenv -> 
-  clausenv
+val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
@@ -107,10 +106,9 @@ 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 :
-  bool -> int option -> evar_info sigma -> constr * constr -> 
-    open_constr bindings -> clausenv
+  evar_info sigma -> int option -> constr * constr -> open_constr bindings ->
+   clausenv
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> open_constr bindings -> clausenv
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 216900bdb..84f9330d3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,21 +120,18 @@ 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 simple_apply_unify_flags = {
+let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = false;
-  use_types = false;
+  use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
 }
 
@@ -726,6 +723,5 @@ 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 *)
-      | _ ->
-	  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
+      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
+
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8cfa20948..1b8f9ccd8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,12 +17,11 @@ 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 simple_apply_unify_flags : unify_flags
+val default_no_delta_unify_flags : unify_flags
 
 (* The "unique" unification fonction *)
 val w_unify :
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index babf53c9f..22dcca289 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -98,7 +98,6 @@ 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 111245e11..0b1f29dc3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -586,7 +586,6 @@ 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 72bc85c2f..4319a1d3d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -72,7 +72,6 @@ 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;
 }
 
@@ -632,7 +631,6 @@ 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;
 }
 
@@ -641,7 +639,6 @@ 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 b5710c966..dc8ff2b9c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,14 +1734,12 @@ 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 1bd65ecdf..dd8aa1294 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 true indbindings indclause in
+  let indclause' = clenv_match_args 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 true elimbindings elimclause' in
+  let elimclause' = clenv_match_args 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 cd8ad4c14..d3f7cc5f1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -551,7 +551,6 @@ 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;
 }
 
@@ -673,10 +672,9 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 
 (* Resolution with missing arguments *)
 
-let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl =
+let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let flags = 
-    if with_delta_and_types then default_unify_flags
-    else simple_apply_unify_flags in
+    if with_delta then default_unify_flags else default_no_delta_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. *)
@@ -686,9 +684,7 @@ let general_apply with_delta_and_types 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 with_delta_and_types (Some n) gl (c,thm_ty) lbind
-    in
+    let clause = make_clenv_binding_apply gl (Some n) (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 ->