diff options
| author | herbelin | 2006-10-28 19:35:09 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-28 19:35:09 +0000 |
| commit | 359e4ffe307d7d8dd250735373fc6354a58ecff5 (patch) | |
| tree | 7204cb80cb272118a7ee60e9790d91d0efd11894 /kernel/declarations.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 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2cbdc3eb39..22cfd62a0c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -26,6 +26,15 @@ type engagement = ImpredicativeSet (**********************************************************************) (*s Representation of constants (Definition/Axiom) *) +type polymorphic_arity = { + poly_param_levels : universe option list; + poly_level : universe; +} + +type constant_type = + | NonPolymorphicType of types + | PolymorphicArity of rel_context * polymorphic_arity + type constr_substituted val from_val : constr -> constr_substituted @@ -34,7 +43,7 @@ val force : constr_substituted -> constr type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; - const_type : types; + const_type : constant_type; const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; @@ -70,11 +79,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths \end{verbatim} *) -type polymorphic_inductive_arity = { - mind_param_levels : universe option list; - mind_level : universe; -} - type monomorphic_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -82,7 +86,7 @@ type monomorphic_inductive_arity = { type inductive_arity = | Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_inductive_arity +| Polymorphic of polymorphic_arity type one_inductive_body = { |