Merge PR #9909: Remove all but one call to `Global` in the pretyper

Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

6 files changed, 70 insertions, 47 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24b1362e6d..b89b6b5765 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -212,7 +212,7 @@ let encode_record r =
 
 module PrintingRecordRecord =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Record"
     let title = "Types leading to pretty-printing using record notation: "
     let member_message s b =
@@ -224,7 +224,7 @@ module PrintingRecordRecord =
 
 module PrintingRecordConstructor =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Constructor"
     let title = "Types leading to pretty-printing using constructor form: "
     let member_message s b =
@@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l
 
 let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
+    Util.List.addn  (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
-  let nb_params = Inductiveops.inductive_nparams ind in
+  let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
       let params,args = Util.List.chop nb_params impls in
@@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi
 let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
-  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
+  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
     let c = extern_reference vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 749eb2289c..3329ba2047 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -643,7 +643,7 @@ let terms_of_binders bl =
     | PatCstr (c,l,_) ->
        let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
-       let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+       let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
        CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
     | bnd :: l ->
@@ -738,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           else
             let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
             match disjpat with
-            | [pat] -> (glob_constr_of_cases_pattern pat, None)
+            | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
             | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
         let terms = Id.Map.fold mk_env terms Id.Map.empty in
@@ -800,7 +800,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       else
         let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
         match disjpat with
-        | [pat] -> glob_constr_of_cases_pattern pat
+        | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
         | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
     with Not_found ->
     try
@@ -1197,10 +1197,10 @@ let check_or_pat_variables loc ids idsl =
     @return if letin are included *)
 let check_constructor_length env loc cstr len_pl pl0 =
   let n = len_pl + List.length pl0 in
-  if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
-    (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
+  if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else
+    (Int.equal n (Inductiveops.constructor_nalldecls env cstr) ||
       (error_wrong_numarg_constructor ?loc env cstr
-         (Inductiveops.constructor_nrealargs cstr)))
+         (Inductiveops.constructor_nrealargs env cstr)))
 
 open Declarations
 
@@ -1226,9 +1226,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with
         have been given in the "explicit" arguments, which come from a
         "@C args" notation or from a custom user notation *)
      let pl' = insert_local_defs_in_pattern cstr pl in
-     let maxargs = Inductiveops.constructor_nalldecls cstr in
+     let maxargs = Inductiveops.constructor_nalldecls env cstr in
      if List.length pl' + List.length args > maxargs then
-       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr);
+       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
      (* Two possibilities: either the args are given with explict
      variables for local definitions, then we give the explicit args
      extended with local defs, so that there is nothing more to be
@@ -1258,15 +1258,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
   in aux 0 (impl_list,pl2)
 
 let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
-  let nargs = Inductiveops.constructor_nallargs c in
-  let nargs' = Inductiveops.constructor_nalldecls c in
+  let nargs = Inductiveops.constructor_nallargs env c in
+  let nargs' = Inductiveops.constructor_nalldecls env c in
   let impls_st = implicits_of_global (ConstructRef c) in
   add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
-  let nallargs = inductive_nallargs_env env c in
-  let nalldecls = inductive_nalldecls_env env c in
+  let nallargs = inductive_nallargs env c in
+  let nalldecls = inductive_nalldecls env c in
   let impls_st = implicits_of_global (IndRef c) in
   add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
@@ -1274,8 +1274,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 =
 (** Do not raise NotEnoughArguments thanks to preconditions*)
 let chop_params_pattern loc ind args with_letin =
   let nparams = if with_letin
-    then Inductiveops.inductive_nparamdecls ind
-    else Inductiveops.inductive_nparams ind in
+    then Inductiveops.inductive_nparamdecls (Global.env()) ind
+    else Inductiveops.inductive_nparams (Global.env()) ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
   List.iter (fun c -> match DAst.get c with
@@ -1295,10 +1295,11 @@ let find_constructor loc add_params ref =
   in
   cstr, match add_params with
     | Some nb_args ->
+      let env = Global.env () in
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
-          then Inductiveops.inductive_nparamdecls ind
-          else Inductiveops.inductive_nparams ind
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr)
+        then Inductiveops.inductive_nparamdecls env ind
+        else Inductiveops.inductive_nparams env ind
       in
       List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
     | None -> []
diff --git a/interp/declare.ml b/interp/declare.ml
index 717f8ef49a..76b4bab2ce 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -346,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = rebuild_inductive }
 
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
+
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
+
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
+  declare_object {
+    (default_object "PRIMPROJS") with
+    cache_function = cache_prim ;
+    load_function = load_prim;
+    subst_function = subst_prim;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_prim }
+
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
+
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
   let univs, u = match univs with
@@ -360,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let entry = definition_entry ~types ~univs term in
   let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  Recordops.declare_primitive_projection p cst
+  declare_primitive_projection p cst
 
 
 let declare_projections univs mind =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 854651e7b7..dffccf02fc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty =
     | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
-	  let c = class_info gr in
-	  let (ci, rd) = c.cl_context in
-	  if not allow_partial then
-	    begin
-              let opt_succ x n = match x with
-              | None -> succ n
-              | Some _ -> n
-              in
-	      let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-	      let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-		if not (Int.equal needlen applen) then
-                  mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-	    end;
-	  let pars = List.rev (List.combine ci rd) in
-	  let args, avoid = combine_params avoid f par pars in
-	    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
-	in c, avoid
+   let env = Global.env () in
+   let sigma = Evd.from_env env in
+   let c = class_info env sigma gr in
+   let (ci, rd) = c.cl_context in
+   if not allow_partial then
+     begin
+       let opt_succ x n = match x with
+         | None -> succ n
+         | Some _ -> n
+       in
+       let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+       let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+       if not (Int.equal needlen applen) then
+         mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+     end;
+   let pars = List.rev (List.combine ci rd) in
+   let args, avoid = combine_params avoid f par pars in
+   CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
+ in c, avoid
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/notation.ml b/interp/notation.ml
index b9aca82cf4..56504db04e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1516,7 +1516,7 @@ let uninterp_prim_token c =
      with Not_found -> raise Notation_ops.No_match
 
 let uninterp_prim_token_cases_pattern c =
-  match glob_constr_of_closed_cases_pattern c with
+  match glob_constr_of_closed_cases_pattern (Global.env()) c with
   | exception Not_found -> raise Notation_ops.No_match
   | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7d7e10a05b..9801e56ca1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function
   | GApp (t, l) ->
     begin match DAst.get t with
     | GRef (ConstructRef cstr,_) ->
-     let nparams = Inductiveops.inductive_nparams (fst cstr) in
+     let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in
      let _,l = List.chop nparams l in
      PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
     | _ -> raise No_match
@@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
 let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
-  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
+  let env = Global.env () in
+  let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
     let patl' = Id.List.assoc var binders in
@@ -1292,7 +1293,7 @@ let match_notation_constr u c (metas,pat) =
     | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
        (match Id.List.assoc x binders with
         | [pat] ->
-          let v = glob_constr_of_cases_pattern pat in
+          let v = glob_constr_of_cases_pattern (Global.env()) pat in
           ((v,scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
     | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
@@ -1333,11 +1334,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+      let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
       sigma,(0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
-      let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
+      let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then