diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-28 19:35:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-28 19:35:09 +0000 |
| commit | 359e4ffe307d7d8dd250735373fc6354a58ecff5 (patch) | |
| tree | 7204cb80cb272118a7ee60e9790d91d0efd11894 /pretyping/retyping.mli | |
| parent | 8bcd34ae13010797a974b0f3c16df6e23f2cb254 (diff) | |
Extension du polymorphisme de sorte au cas des définitions dans Type.
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 900a96829..32b90cd86 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -36,3 +36,6 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types + +val type_of_constant_knowing_parameters : env -> evar_map -> constant -> + constr array -> types |