Unify meta types with the right flags, add betaiotazeta reduction to unification (potentially harmful)

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

2 files changed, 28 insertions, 10 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d2ee780c6a..50b1c61396 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -316,20 +316,34 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		  array_fold_left2 (unirec_rec curenvnb topconv true)
 		    (unirec_rec curenvnb pb true substn f1 f2) l1 l2
 		with ex when precatchable_exception ex ->
-		  try expand curenvnb pb b substn cM f1 l1 cN f2 l2
+		  try reduce curenvnb pb b substn cM cN
 		  with ex when precatchable_exception ex ->
-		    canonical_projections curenvnb pb b cM cN substn)
+		    try expand curenvnb pb b substn cM f1 l1 cN f2 l2
+		    with ex when precatchable_exception ex ->
+		      canonical_projections curenvnb pb b cM cN substn)
 
 	| _ ->
 	    try canonical_projections curenvnb pb b cM cN substn
 	    with ex when precatchable_exception ex ->
               if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
-		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 curenvnb pb b substn cM f1 l1 cN f2 l2
-
+ 		try reduce curenvnb pb b substn cM cN
+		with ex when precatchable_exception ex ->
+		  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 curenvnb pb b substn cM f1 l1 cN f2 l2
+
+  and reduce curenvnb pb b (sigma, _, _ as substn) cM cN =
+    let cM' = whd_betaiotazeta sigma cM in
+      if not (eq_constr cM cM') then
+	unirec_rec curenvnb pb true substn cM' cN
+      else
+	let cN' = whd_betaiotazeta sigma cN in
+	  if not (eq_constr cN cN') then
+	    unirec_rec curenvnb pb true substn cM cN'
+	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
+	    
   and expand (curenv,_ as curenvnb) pb b (sigma,metasubst,_ as substn) cM f1 l1 cN f2 l2 =
 
     if
@@ -633,7 +647,11 @@ let unify_to_type env sigma flags c status u =
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
-    unify_to_type env sigma flags c status mvty
+  let mvty = nf_meta sigma mvty in
+    unify_to_type env sigma 
+      {flags with modulo_delta = flags.modulo_delta_types;
+	 modulo_conv_on_closed_terms = Some flags.modulo_delta_types}
+      c status mvty
 
 (* Move metas that may need coercion at the end of the list of instances *)
 
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index eddf1dd04f..f23b9f178e 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -70,7 +70,7 @@ Proof.
   rewrite Rinv_mult_distr.
   repeat rewrite Rmult_assoc.
   apply Rmult_eq_compat_l.
-  pattern x at 2 in |- *; rewrite Rmult_comm.
+  rewrite Rmult_comm. 
   repeat rewrite Rmult_assoc.
   apply Rmult_eq_compat_l.
   reflexivity.