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/logic.ml | |
| 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/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |