Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clause of an inductive definitions

6 files changed, 32 insertions, 32 deletions

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