diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 18 | ||||
| -rw-r--r-- | interp/declare.ml | 24 |
2 files changed, 20 insertions, 22 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6e98da1c04..37394386e6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -650,7 +650,7 @@ example of recursive notation with closed binders: A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example: -.. coqtop:: in +.. coqtop:: in Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) @@ -1137,7 +1137,7 @@ The ``function_scope`` interpretation scope .. index:: function_scope -The scope ``function_scope`` also has a special status. +The scope ``function_scope`` also has a special status. It is temporarily activated each time the argument of a global reference is recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or :g:`A -> B`. @@ -1152,11 +1152,11 @@ Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It - is delimited by key ``type``, and bound to the coercion class + is delimited by key ``type``, and bound to the coercion class ``Sortclass``, as described above. ``function_scope`` - This scope is delimited by key ``function``, and bound to the coercion class + This scope is delimited by key ``function``, and bound to the coercion class ``Funclass``, as described above. ``nat_scope`` @@ -1455,7 +1455,9 @@ tactic language. Tactic notations obey the following syntax: .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as ``no associative`` but the parser on - which Coq is built, namely Camlp4, currently does not implement the - ``no associativity`` and replaces it by a ``left associativity``; hence it is - the same for Coq: ``no associativity`` is in fact ``left associativity``. +.. [#no_associativity] Coq accepts notations declared as ``no + associativity`` but the parser on which Coq is built, namely + Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for + Coq: ``no associativity`` is in fact ``left associativity``, for + the purposes of parsing diff --git a/interp/declare.ml b/interp/declare.ml index 532339c03c..2b2ca36edc 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -471,24 +471,20 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -(** Global universe names, in a different summary *) +(** Monomorphic universes need to survive sections. *) -type universe_context_decl = polymorphic * Univ.ContextSet.t - -let cache_universe_context (p, ctx) = - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx - -let input_universe_context : universe_context_decl -> Libobject.obj = +let input_universe_context : Univ.ContextSet.t -> Libobject.obj = declare_object - { (default_object "Global universe context state") with - cache_function = (fun (na, pi) -> cache_universe_context pi); - load_function = (fun _ (_, pi) -> cache_universe_context pi); - discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); - classify_function = (fun a -> Keep a) } + { (default_object "Monomorphic section universes") with + cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); + discharge_function = (fun (_, x) -> Some x); + classify_function = (fun a -> Dispose) } let declare_universe_context poly ctx = - Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + if poly then + (Global.push_context_set true ctx; Lib.add_section_context ctx) + else + Lib.add_anonymous_leaf (input_universe_context ctx) (** Global universes are not substitutive objects but global objects bound at the *library* or *module* level. The polymorphic flag is |