From dfe97724fb6034fc06b3ef693f6a3ed94733adbc Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 29 Oct 2006 20:11:08 +0000 Subject: Compatibilité du polymorphisme de constantes avec les sections. Amélioration affichage des univers. Réparation de petits oublis du premier commit. Essai d'une nouvelle stratégie : si le type d'une constante est mentionné explicitement, la constante est monomorphe dans Type. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/retyping.mli | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'pretyping/retyping.mli') diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 32b90cd86..6dbd426b2 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -34,8 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types (* Makes an unsafe judgment from a constr *) 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 -> +val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types + -- cgit v1.2.3