diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 5 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index af118b5f1d..8df0858910 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -73,10 +73,11 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in + let evd = Evd.solve_sort_constraints clenv.evd in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd - else clenv.evd + Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env evd + else evd in tclTHEN (tclEVARS ( evd')) diff --git a/proofs/logic.ml b/proofs/logic.ml index 5f164b020f..2cca258b95 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -321,7 +321,7 @@ let check_conv_leq_goal env sigma arg ty conclty = raise (RefinerError (BadType (arg,ty,conclty))) let goal_type_of env sigma c = - (if !check then type_of else Retyping.get_type_of) env sigma c + (if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = let env = evar_env goal in |