diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-23 19:36:19 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-23 19:36:19 +0000 |
| commit | 8220bfabb8bcbc29d6b0ac6b5cf8f18e08bc868a (patch) | |
| tree | 85f600d805a015b3596ad141404a933b4e1a8594 /proofs | |
| parent | 3b585059c16dbfbd0558196549d1130509611b35 (diff) | |
A try at using sort variables during unification. Instead of refreshing
universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort
constraints are thrown away at the end of unification for the moment,
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
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 af118b5f1..8df085891 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 5f164b020..2cca258b9 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 |