From 26f216653aed171a70513d3f5ece059ab30bcd73 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Oct 2017 23:55:54 +0200 Subject: Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.). This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause. --- vernac/metasyntax.mli | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'vernac/metasyntax.mli') diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 9cd00cbcb..b3049f1b7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -11,15 +11,16 @@ open Vernacexpr open Notation open Constrexpr open Notation_term +open Environ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> (lstring * syntax_modifier list) -> +val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> constr_expr -> +val add_notation : locality_flag -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -33,11 +34,11 @@ val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : - (lstring * constr_expr * scope_name option) -> unit + env -> (lstring * constr_expr * scope_name option) -> unit (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.internalization_env -> +val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (** Add only the parsing/printing rule of a notation *) @@ -47,7 +48,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> +val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) -- cgit v1.2.3