- Improve unification (beta-reduction, and same heuristic as evarconv for reducing matches).

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

3 files changed, 15 insertions, 8 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 50b1c61396..1bbecc4e2d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -225,6 +225,10 @@ let oracle_order env cf1 cf2 =
       | None -> Some true
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
 
+let do_reduce env sigma c =
+  let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in
+    applist (t, list_of_stack l)
+
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
@@ -284,9 +288,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            array_fold_left2 (unirec_rec curenvnb topconv true)
-	      (unirec_rec curenvnb topconv true
-		  (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
+            (try 
+	       array_fold_left2 (unirec_rec curenvnb topconv true)
+		 (unirec_rec curenvnb topconv true
+		    (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
+	     with ex when precatchable_exception ex ->
+	       reduce curenvnb pb b substn cM cN)
 
 	| App (f1,l1), _ when
 	    (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) &
@@ -335,11 +342,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		    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
+    let cM' = do_reduce (fst curenvnb) 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
+	let cN' = do_reduce (fst curenvnb) 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)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d7ead8b7ed..4dfe035007 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -354,7 +354,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 	       (fun {it=gls';sigma=s'} fk' ->
 		  let needs_backtrack = 
 		    if gls' = [] then
-		      dependent info.only_classes s' info.is_evar (Goal.V82.concl s' gl)
+ 		      dependent info.only_classes s' info.is_evar (Goal.V82.concl s gl)
 		    else true
 		  in
 		  let fk'' = if not needs_backtrack then
@@ -586,7 +586,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	then (* Unable to satisfy the constraints. *)
 	  error_unresolvable env comp do_split evd
 	else (* Best effort: do nothing on this component *) 
-	  docomp oevd comps
+	  docomp evd comps
   in docomp oevd split
 
 let initial_select_evars onlyargs =
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 86385a8526..dd97b865d4 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -646,7 +646,7 @@ Proof.
   apply H3.
   rewrite Rminus_0_r; apply Rabs_right.
   apply Rle_ge.
-  unfold Rdiv in |- *; repeat apply Rmult_le_pos.
+  unfold Rdiv in |- *; apply Rmult_le_pos. 
   apply pow_le.
   apply Rle_trans with 1.
   left; apply Rlt_0_1.