diff options
| author | msozeau | 2009-05-23 19:36:19 +0000 |
|---|---|---|
| committer | msozeau | 2009-05-23 19:36:19 +0000 |
| commit | 8220bfabb8bcbc29d6b0ac6b5cf8f18e08bc868a (patch) | |
| tree | 85f600d805a015b3596ad141404a933b4e1a8594 /pretyping/retyping.mli | |
| 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 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index be42fd8585..9b65494c1e 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -21,7 +21,7 @@ open Environ either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -val get_type_of : env -> evar_map -> constr -> types +val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types val get_sort_of : env -> evar_map -> types -> sorts val get_sort_family_of : env -> evar_map -> types -> sorts_family |