aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/constrintern.mli2
-rw-r--r--test-suite/bugs/closed/5762.v28
-rw-r--r--test-suite/coqdoc/links.html.out2
-rw-r--r--test-suite/coqdoc/links.tex.out2
-rw-r--r--vernac/command.ml11
-rw-r--r--vernac/metasyntax.ml32
-rw-r--r--vernac/metasyntax.mli11
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml6
11 files changed, 64 insertions, 38 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cea307d7..a0a749bfb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2132,8 +2132,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
~pattern_mode:true ~ltacvars env c in
pattern_of_glob_constr c
-let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
- let env = Global.env () in
+let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
@@ -2212,4 +2211,3 @@ let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_
let int_env,bl = intern_context global_level env impl_env params in
let x = interp_glob_context_evars env evdref shift bl in
int_env, x
-
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0a4eaf838..75e99dd9b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -182,7 +182,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
-val interp_notation_constr : ?impls:internalization_env ->
+val interp_notation_constr : env -> ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes * notation_var_internalization_type) Id.Map.t *
notation_constr * reversibility_flag
diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v
new file mode 100644
index 000000000..edd5c8d73
--- /dev/null
+++ b/test-suite/bugs/closed/5762.v
@@ -0,0 +1,28 @@
+(* Supporting imp. params. in inductive or fixpoints mutually defined with a notation *)
+
+Reserved Notation "* a" (at level 70).
+Inductive P {n : nat} : nat -> Prop :=
+| c m : *m
+where "* m" := (P m).
+
+Reserved Notation "##".
+Inductive I {A:Type} := C : ## where "##" := I.
+
+(* The following was working in 8.6 *)
+
+Require Import Vector.
+
+Reserved Notation "# a" (at level 70).
+Fixpoint f {n : nat} (v:Vector.t nat n) : nat :=
+ match v with
+ | nil _ => 0
+ | cons _ _ _ v => S (#v)
+ end
+where "# v" := (f v).
+
+(* The following was working in 8.6 *)
+
+Reserved Notation "%% a" (at level 70).
+Record R :=
+ {g : forall {A} (a:A), a=a where "%% x" := (g x);
+ k : %% 0 = eq_refl}.
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index 7d7d01c1b..e2928f78d 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -76,7 +76,7 @@ Various checks for coqdoc
<br/>
<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/>
<br/>
-<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="variable">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
+<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 844fb3031..de3182d1a 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -59,7 +59,7 @@ Various checks for coqdoc
\coqdocnoindent
\coqdoceol
\coqdocnoindent
-\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
diff --git a/vernac/command.ml b/vernac/command.ml
index f095a5d6c..f58ed065c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -550,13 +550,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
- let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
Metasyntax.with_syntax_protection (fun () ->
(* Temporary declaration of notations and scopes *)
- List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations;
+ List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations;
(* Interpret the constructor types *)
List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
() in
@@ -708,7 +707,7 @@ let do_mutual_inductive indl cum poly prv finite =
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
- List.iter Metasyntax.add_notation_interpretation ntns;
+ List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
(* If positivity is assumed declares itself as unsafe. *)
@@ -1110,7 +1109,7 @@ let interp_recursive isfix fixl notations =
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
Metasyntax.with_syntax_protection (fun () ->
- List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
+ List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
List.map4
(fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls))
fixctximpenvs fixctxs fixl fixccls)
@@ -1176,7 +1175,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
fixpoint_message (Some indexes) fixnames;
end;
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
@@ -1207,7 +1206,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
cofixpoint_message fixnames
end;
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
let extract_decreasing_argument limit = function
| (na,CStructRec) -> na
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index b2d48bb2f..9376afa8c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1318,7 +1318,7 @@ let to_map l =
let fold accu (x, v) = Id.Map.add x v accu in
List.fold_left fold Id.Map.empty l
-let add_notation_in_scope local df c mods scope =
+let add_notation_in_scope local df env c mods scope =
let open SynData in
let sd = compute_syntax_data df mods in
(* Prepare the interpretation *)
@@ -1329,7 +1329,7 @@ let add_notation_in_scope local df c mods scope =
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map sd.recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr env nenv c in
let interp = make_interpretation_vars sd.recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in
@@ -1349,7 +1349,7 @@ let add_notation_in_scope local df c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
sd.info
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
@@ -1368,7 +1368,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable onlyparse (not reversible) ac in
@@ -1395,33 +1395,33 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in
(* Notations with only interpretation *)
-let add_notation_interpretation ((loc,df),c,sc) =
- let df' = add_notation_interpretation_core false df c sc false false None in
+let add_notation_interpretation env ((loc,df),c,sc) =
+ let df' = add_notation_interpretation_core false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
-let set_notation_for_interpretation impls ((_,df),c,sc) =
+let set_notation_for_interpretation env impls ((_,df),c,sc) =
(try ignore
- (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
(* Main entry point *)
-let add_notation local c ((loc,df),modifiers) sc =
+let add_notation local env c ((loc,df),modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
let compat = get_compat_version modifiers in
- try add_notation_interpretation_core local df c sc onlyparse onlyprint compat
+ try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
- add_notation_in_scope local df c modifiers sc
+ add_notation_in_scope local df env c modifiers sc
else
(* Declare both syntax and interpretation *)
- add_notation_in_scope local df c modifiers sc
+ add_notation_in_scope local df env c modifiers sc
in
Dumpglob.dump_notation (loc,df') sc true
@@ -1436,13 +1436,13 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
-let add_infix local ((loc,inf),modifiers) pr sc =
+let add_infix local env ((loc,inf),modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let metas = [inject_var "x"; inject_var "y"] in
let c = mkAppC (pr,metas) in
let df = "x "^(quote_notation_token inf)^" y" in
- add_notation local c ((loc,df),modifiers) sc
+ add_notation local env c ((loc,df),modifiers) sc
(**********************************************************************)
(* Delimiters and classes bound to scopes *)
@@ -1498,7 +1498,7 @@ let try_interp_name_alias = function
| [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
-let add_syntactic_definition ident (vars,c) local onlyparse =
+let add_syntactic_definition env ident (vars,c) local onlyparse =
let nonprintable = ref false in
let vars,pat =
try [], NRef (try_interp_name_alias (vars,c))
@@ -1509,7 +1509,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
} in
- let nvars, pat, reversible = interp_notation_constr nenv c in
+ let nvars, pat, reversible = interp_notation_constr env nenv c in
let () = nonprintable := not reversible in
let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
List.map map vars, pat
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 *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 81218308f..785c842ba 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -556,7 +556,7 @@ let declare_mutual_definition l =
let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
- List.iter Metasyntax.add_notation_interpretation first.prg_notations;
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
diff --git a/vernac/record.ml b/vernac/record.ml
index 18e7796ca..9a8657c3c 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -72,7 +72,7 @@ let interp_fields_evars env evars impls_env nots l =
| None -> LocalAssum (i,t')
| Some b' -> LocalDef (i,b',t')
in
- List.iter (Metasyntax.set_notation_for_interpretation impls) no;
+ List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
(EConstr.push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], impls_env) nots l
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b7a861214..e08cb8387 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -430,11 +430,11 @@ let vernac_arguments_scope locality r scl =
let vernac_infix locality local =
let local = enforce_module_locality locality local in
- Metasyntax.add_infix local
+ Metasyntax.add_infix local (Global.env())
let vernac_notation locality local =
let local = enforce_module_locality locality local in
- Metasyntax.add_notation local
+ Metasyntax.add_notation local (Global.env())
(***********)
(* Gallina *)
@@ -953,7 +953,7 @@ let vernac_hints locality poly local lb h =
let vernac_syntactic_definition locality lid x local y =
Dumpglob.dump_definition lid false "syndef";
let local = enforce_module_locality locality local in
- Metasyntax.add_syntactic_definition (snd lid) x local y
+ Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
let vernac_declare_implicits locality r l =
let local = make_section_locality locality in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 08:23:26 +0000