Essai de prise en compte de delta dans unify_0 (même sur termes non clos).

- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
  d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
  désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
  d'unification initial. C'est une heuristique qui est intuitive mais qui
  reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
  peu moins d'1%.



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

9 files changed, 129 insertions, 54 deletions

diff --git a/CHANGES b/CHANGES
index 926b7002d..817978b74 100644
--- a/CHANGES
+++ b/CHANGES
@@ -96,7 +96,6 @@ Tactic Language
   hence, the "rec" keyword can be used to turn the argument of a
   "let ... in ..." into a lazy one.
 
-
 Tactics
 
 - New tactics [apply -> term], [apply <- term], [apply -> term in
@@ -122,6 +121,9 @@ Tactics
 - New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
 - New tactic "dependent induction H [ generalizing id_1 .. id_n ]" to do 
   induction-inversion on instantiated inductive families à la BasicElim.
+- 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).
 
 Type Classes
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 74024779a..77098a5c3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -96,6 +96,13 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
 	metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
     | _ -> assert false
 
+let expand_constant env c = 
+  let (ids,csts) = Conv_oracle.freeze() in
+  match kind_of_term c with
+  | Const cst when Cpred.mem cst csts -> constant_opt_value env cst
+  | Var id when Idpred.mem id ids -> named_body id env
+  | _ -> None
+
 (*******************************)
 
 (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -116,20 +123,28 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
-type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool }
+type unify_flags = { 
+  modulo_conv_on_closed_terms : bool; 
+  use_metas_eagerly : bool;
+  modulo_conv : bool
+}
 
-let default_unify_flags = { modulo_delta = true; use_metas_eagerly = true }
+let default_unify_flags = {
+  modulo_conv_on_closed_terms = true;
+  use_metas_eagerly = true;
+  modulo_conv = true 
+}
 
-let unify_0_with_initial_metas metas env sigma cv_pb flags m n =
+let unify_0_with_initial_metas metas is_subterm env sigma cv_pb flags m n =
   let nb = nb_rel env in
-  let trivial_unify pb (metasubst,_ as substn) m n =
-    let metas = if flags.use_metas_eagerly then metasubst else metas in
+  let trivial_unify pb (metasubst,_) m n =
     match subst_defined_metas metas m with
-      | Some m when
-	  (if flags.modulo_delta then is_fconv (conv_pb_of pb) env sigma m n
-	  else eq_constr m n) -> substn
-      | _ -> error_cannot_unify env sigma (m,n) in
-  let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
+    | Some m ->
+	if flags.modulo_conv_on_closed_terms 
+	then is_fconv (conv_pb_of pb) env sigma m n
+	else eq_constr m n
+    | _ -> false in
+  let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
     and cN = Evarutil.whd_castappevar sigma curn in 
       match (kind_of_term cM,kind_of_term cN) with
@@ -152,14 +167,19 @@ let unify_0_with_initial_metas metas env sigma cv_pb flags m n =
 	| Evar ev, _ -> metasubst,((ev,cN)::evarsubst)
 	| _, Evar ev -> metasubst,((ev,cM)::evarsubst)
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
-	    unirec_rec (push_rel_assum (na,t1) curenv) topconv
-	      (unirec_rec curenv topconv substn t1 t2) c1 c2
+	    unirec_rec (push_rel_assum (na,t1) curenv) topconv true
+	      (unirec_rec curenv topconv true substn t1 t2) c1 c2
 	| Prod (na,t1,c1), Prod (_,t2,c2) ->
-	    unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb)
-	      (unirec_rec curenv topconv substn t1 t2) c1 c2
-	| LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN
-	| _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c)
+	    unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb) true
+	      (unirec_rec curenv topconv true substn t1 t2) c1 c2
+	| LetIn (_,a,_,c), _ -> unirec_rec curenv pb b substn (subst1 a c) cN
+	| _, LetIn (_,a,_,c) -> unirec_rec curenv pb b substn cM (subst1 a c)
 	    
+	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+            array_fold_left2 (unirec_rec curenv topconv true)
+	      (unirec_rec curenv topconv true
+		  (unirec_rec curenv topconv true substn p1 p2) c1 c2) cl1 cl2
+
 	| App (f1,l1), _ when
 	    isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenv f1 l1 cN substn
@@ -171,36 +191,53 @@ let unify_0_with_initial_metas metas env sigma cv_pb flags m n =
 	| App (f1,l1), App (f2,l2) ->
 	      let len1 = Array.length l1
 	      and len2 = Array.length l2 in
-              let (f1,l1,f2,l2) =
-		if len1 = len2 then (f1,l1,f2,l2)
-		else if len1 < len2 then
-		  let extras,restl2 = array_chop (len2-len1) l2 in 
-		    (f1, l1, appvect (f2,extras), restl2)
-		else 
-		  let extras,restl1 = array_chop (len1-len2) l1 in 
-		    (appvect (f1,extras), restl1, f2, l2) in
-	      let pb = ConvUnderApp (len1,len2) in
-		(try
-		    array_fold_left2 (unirec_rec curenv topconv)
-		      (unirec_rec curenv pb substn f1 f2) l1 l2
+	      (try
+		  let (f1,l1,f2,l2) =
+		    if len1 = len2 then (f1,l1,f2,l2)
+		    else if len1 < len2 then
+		      let extras,restl2 = array_chop (len2-len1) l2 in 
+		      (f1, l1, appvect (f2,extras), restl2)
+		    else 
+		      let extras,restl1 = array_chop (len1-len2) l1 in 
+		      (appvect (f1,extras), restl1, f2, l2) in
+		  let pb = ConvUnderApp (len1,len2) in
+		  array_fold_left2 (unirec_rec curenv topconv true)
+		    (unirec_rec curenv pb true substn f1 f2) l1 l2
 		  with ex when precatchable_exception ex ->
-		    trivial_unify pb substn cM cN)
-	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            array_fold_left2 (unirec_rec curenv topconv)
-	      (unirec_rec curenv topconv
-		  (unirec_rec curenv topconv substn p1 p2) c1 c2) cl1 cl2
-	| _ -> trivial_unify pb substn cM cN
+		    expand curenv pb b substn cM f1 l1 cN f2 l2)
+
+	| _ -> 
+	    let (f1,l1) = 
+	      match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
+	    let (f2,l2) =
+	      match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
+	    expand curenv pb b substn cM f1 l1 cN f2 l2
+
+  and expand curenv pb b substn cM f1 l1 cN f2 l2 =
+    if trivial_unify pb substn cM cN then substn
+    else if b & flags.modulo_conv then
+      match expand_constant curenv f1 with
+      | Some c ->
+	  unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+      | None ->
+      match expand_constant curenv f2 with
+      | Some c ->
+	  unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+      | None ->
+      error_cannot_unify env sigma (cM,cN)
+    else
+      error_cannot_unify env sigma (cM,cN)
+
   in
     if (not(occur_meta m)) &&
-      (if flags.modulo_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
+      (if flags.modulo_conv then is_fconv (conv_pb_of cv_pb) env sigma m n
        else eq_constr m n)
     then 
       (metas,[])
     else 
-      let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in
-	((*sort_eqns*) mc, (*sort_eqns*) ec)
+      unirec_rec env cv_pb is_subterm (metas,[]) m n
 
-let unify_0 = unify_0_with_initial_metas []
+let unify_0 = unify_0_with_initial_metas [] true
 
 let left = true
 let right = false
@@ -482,7 +519,7 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
 let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let (mc2,ec) = 
-    unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb flags m n
+    unify_0_with_initial_metas mc1 false env (evars_of evd') cv_pb flags m n
   in 
   w_merge env with_types flags mc2 ec evd'
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f0717b2a7..e59869428 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -14,7 +14,11 @@ open Environ
 open Evd
 (*i*)
 
-type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool }
+type unify_flags = { 
+  modulo_conv_on_closed_terms : bool; 
+  use_metas_eagerly : bool;
+  modulo_conv : bool
+}
 
 val default_unify_flags : unify_flags
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ad19bd9b6..ced684965 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -67,15 +67,17 @@ let clenv_refine with_evars clenv gls =
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
+let dft = Unification.default_unify_flags
 
-let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls =
-  clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls
+let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls =
+  clenv_refine with_evars
+    (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls
 
-let elim_res_pf_THEN_i clenv tac gls =  
+let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver true clenv gls) in
   tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -83,11 +85,19 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
+open Unification
+
+let fail_quick_unif_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = false;
+  modulo_conv = false; 
+}
+
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unifyTerms m n gls = 
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
-  let evd' = Unification.w_unify false env CONV m n evd in
+  let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
 let unify m gls =
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 038f84f01..90d010c80 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -17,12 +17,13 @@ open Evd
 open Clenv
 open Proof_type
 open Tacexpr
+open Unification
 (*i*)
 
 (* Tactics *)
 val unify : constr -> tactic
 val clenv_refine : evars_flag -> clausenv -> tactic
-val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic
+val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
 (* Compatibility, use res_pf ?with_evars:true instead *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index ebba4b00b..92786e089 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -561,7 +561,11 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
 open Unification
 
-let auto_unif_flags = { modulo_delta = true; use_metas_eagerly = false }
+let auto_unif_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = false;
+  modulo_conv = false; 
+}
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index fb25d9d25..0214a940c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1731,8 +1731,17 @@ let check_evar_map_of_evars_defs evd =
 (* [unification_rewrite] searchs a match for [c1] in [but] and then 
    returns the modified objects (in particular [c1] and [c2]) *)  
 
-let rewrite_unif_flags = { modulo_delta = false; use_metas_eagerly = true }
-let rewrite2_unif_flags = { modulo_delta = true; use_metas_eagerly = true }
+let rewrite_unif_flags = {
+  modulo_conv_on_closed_terms = false;
+  use_metas_eagerly = true;
+  modulo_conv = false
+}
+
+let rewrite2_unif_flags = {
+  modulo_conv_on_closed_terms = true;
+  use_metas_eagerly = true;
+  modulo_conv = false
+ }
 
 let unification_rewrite c1 c2 cl but gl = 
   let (env',c1) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 39765526f..fa40e1651 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,7 @@ open Decl_kinds
 open Evarutil
 open Indrec
 open Pretype_errors
+open Unification
 
 exception Bound
 
@@ -822,7 +823,13 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  
       array_last cl
   | _ -> anomaly "last_arg"
-	
+
+let elim_flags = {
+  modulo_conv_on_closed_terms = true; 
+  use_metas_eagerly = true;
+  modulo_conv = false
+}
+
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg elimclause.templval.rebus) with
@@ -831,7 +838,8 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K gl
+  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
+    gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 2fb6b2265..f792b84d1 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -560,9 +560,9 @@ Proof.
       | apply Rlt_le_trans with (Rmin delta1 delta2);
         [ assumption | apply Rmin_l ] ].
   change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *;
-    repeat rewrite Rmult_assoc; repeat apply Rmult_lt_0_compat.
+    repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat.
   assumption.
-  apply Rsqr_pos_lt; assumption.
+  apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption.
   apply Rinv_0_lt_compat; cut (0%nat <> 2%nat);
     [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *;
       intro; assumption