diff options
| -rw-r--r-- | pretyping/unification.ml | 17 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 | ||||
| -rw-r--r-- | theories/Reals/Exp_prop.v | 2 |
3 files changed, 15 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 50b1c6139..1bbecc4e2 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 d7ead8b7e..4dfe03500 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 86385a852..dd97b865d 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. |