diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-29 20:11:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-29 20:11:08 +0000 |
| commit | dfe97724fb6034fc06b3ef693f6a3ed94733adbc (patch) | |
| tree | 673d36afb27326fe8bd5a5165203a8199405833d /pretyping/termops.mli | |
| parent | 631769875f5a7e099cf814ac7b1aaab624f40a9d (diff) | |
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.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index c635dc887..d461498d9 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -204,6 +204,8 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t (* Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool +val isGlobalRef : constr -> bool + (* Combinators on judgments *) val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment |