diff options
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 1 |
3 files changed, 11 insertions, 11 deletions
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 47882e771..b49190d44 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -575,15 +575,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in (pretype tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val in - evdref := consider_remaining_unif_problems env !evdref; - if resolve_classes then - (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false + (pretype_type empty_valcon env evdref lvar c).utj_val + in + if resolve_classes then + evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; - evdref := consider_remaining_unif_problems env !evdref); - let c = if expand_evar then nf_evar !evdref c' else c' in - if fail_evar then check_evars env Evd.empty !evdref c; - c + evdref := consider_remaining_unif_problems env !evdref; + let c = if expand_evar then nf_evar !evdref c' else c' in + if fail_evar then check_evars env Evd.empty !evdref c; + c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bed4d834d..013270a6a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -677,7 +677,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env evdref lvar c).utj_val in if resolve_classes then ( - evdref := consider_remaining_unif_problems env !evdref; evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref); @@ -694,10 +693,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in - let evd = consider_remaining_unif_problems env !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false - ~fail:true env evd + ~fail:true env !evdref in + let evd = consider_remaining_unif_problems env evd in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 79c9bec53..c3c5f9c95 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -324,6 +324,7 @@ Ltac simplify_one_dep_elim_term c := refine (simplification_existT2 _ _ _ _ _ _ _) || refine (simplification_existT1 _ _ _ _ _ _ _ _) | ?x = ?y -> _ => (* variables case *) + (unfold x) || (unfold y) || (let hyp := fresh in intros hyp ; move hyp before x ; revert_until hyp ; generalize dependent x ; refine (solution_left _ _ _ _)(* ; intros until 0 *)) || |