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.

1 files changed, 5 insertions, 6 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 120f9590f2..1668a93f15 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -549,13 +549,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
@@ -707,7 +706,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. *)
@@ -1109,7 +1108,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)
@@ -1175,7 +1174,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
@@ -1206,7 +1205,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