Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.

8 files changed, 36 insertions, 41 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0533d0d43..cd5eff4e7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -52,7 +52,7 @@ let _ =
        let open Vernacexpr in
        { info with hint_pattern =
 		   Option.map
-		     (Constrintern.intern_constr_pattern (Global.env()))
+                     (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
 		     info.hint_pattern } in
      Flags.silently (fun () ->
 	Hints.add_hints local [typeclasses_db]
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 7e5b941ad..9fd2153cb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Vars
-open Environ
 open Declare
 open Names
 open Globnames
@@ -87,7 +86,6 @@ match local with
 let interp_assumption sigma env impls bl c =
   let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
   let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
-  let ty = EConstr.Unsafe.to_constr ty in
   sigma, (ty, impls)
 
 (* When monomorphic the universe constraints are declared with the first declaration only. *)
@@ -151,9 +149,9 @@ let do_assumptions kind nl l =
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
     let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
     let env =
-      push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+      EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
-      let impls = compute_internalization_data env Variable t imps in
+      let impls = compute_internalization_data env sigma Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
       ((sigma,env,ienv),((is_coe,idl),t,imps)))
     (sigma,env,empty_internalization_env) l
@@ -161,7 +159,7 @@ let do_assumptions kind nl l =
   let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
   (* The universe constraints come from the whole telescope. *)
   let sigma = Evd.nf_constraints sigma in
-  let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in
+  let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
       let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 489f299a2..edfe7aa81 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -212,8 +212,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in
-  let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
+  let impls = compute_internalization_env env sigma Recursive fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let sigma, fixdefs =
@@ -226,10 +225,9 @@ let interp_recursive ~program_mode ~cofix fixl notations =
 
   (* Instantiate evars and check all are resolved *)
   let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
-  let sigma, nf = nf_evars_and_universes sigma in
-  let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in
-  let fixdefs = List.map (Option.map nf) fixdefs in
-  let fixtypes = List.map nf fixtypes in
+  let sigma, _ = nf_evars_and_universes sigma in
+  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
+  let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index c650e9e40..cef5546c6 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -11,7 +11,6 @@ open CErrors
 open Sorts
 open Util
 open Constr
-open Termops
 open Environ
 open Declare
 open Names
@@ -51,7 +50,7 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   )
 
 let push_types env idl tl =
-  List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env)
+  List.fold_left2 (fun env id t -> EConstr.push_rel (LocalAssum (Name id,t)) env)
     env idl tl
 
 type structured_one_inductive_expr = {
@@ -90,7 +89,7 @@ let check_all_names_different indl =
   | _ -> raise (InductiveError (SameNamesOverlap l))
 
 let mk_mltype_data sigma env assums arity indname =
-  let is_ml_type = is_sort env sigma (EConstr.of_constr arity) in
+  let is_ml_type = is_sort env sigma arity in
   (is_ml_type,indname,assums)
 
 let prepare_param = function
@@ -130,14 +129,13 @@ let is_impredicative env u =
   u = Prop Null || (is_impredicative_set env && u = Prop Pos)
 
 let interp_ind_arity env sigma ind =
-  let c = intern_gen IsType env ind.ind_arity in
+  let c = intern_gen IsType env sigma ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
   let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
   let pseudo_poly = check_anonymous_type c in
   let () = if not (Reductionops.is_arity env sigma t) then
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
   in
-  let t = EConstr.Unsafe.to_constr t in
   sigma, (t, pseudo_poly, impls)
 
 let interp_cstrs env sigma impls mldata arity ind =
@@ -272,7 +270,6 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
     interp_context_evars env0 sigma paramsl
   in
-  let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -282,16 +279,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   (* Interpret the arities *)
   let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
 
-  let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in
+  let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
   let env_ar = push_types env0 indnames fullarities in
-  let env_ar_params = push_rel_context ctx_params env_ar in
+  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, _, impls) -> userimpls @
     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 ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in
+  let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
+  let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
 
   let sigma, constructors =
@@ -306,15 +303,14 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
   (* Compute renewed arities *)
   let sigma, nf = nf_evars_and_universes sigma in
-  let arities = List.map nf arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
+  let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
   let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
   let sigma, nf' = nf_evars_and_universes sigma in
-  let nf x = nf' (nf x) in
   let arities = List.map nf' arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
-  let ctx_params = Context.Rel.map nf ctx_params in
+  let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
   List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
   Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index af34f8b29..bd7ee0978 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -171,8 +171,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let sigma, intern_body =
     let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
-      Constrintern.compute_internalization_data env
-        Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls
+      Constrintern.compute_internalization_data env sigma
+        Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
         (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e4bcbc4bb..6447fc350 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -816,13 +816,13 @@ let solve_by_tac name evi t poly ctx =
   let id = name in
   let concl = EConstr.of_constr evi.evar_concl in
   (* spiwack: the status is dropped. *)
-  let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
+  let (entry,_,ctx') = Pfedit.build_constant_by_tactic
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
   let body, () = Future.force entry.const_entry_body in
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
-  Inductiveops.control_only_guard (Global.env ()) (fst body);
+  Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
   (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
 
 let obligation_terminator name num guard hook auto pf =
@@ -838,7 +838,7 @@ let obligation_terminator name num guard hook auto pf =
     let (body, cstr), () = Future.force entry.Entries.const_entry_body in
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
-    Inductiveops.control_only_guard (Global.env ()) body;
+    Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (** Declare the obligation ourselves and drop the hook *)
     let prg = get_info (ProgMap.find name !from_prg) in
     (** Ensure universes are substituted properly in body and type *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1140e3d37..44113bfad 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -70,7 +70,7 @@ let interp_fields_evars env sigma impls_env nots l =
       let impls =
 	match i with
 	| Anonymous -> impls
-        | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls
+        | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
       in
       let d = match b' with
 	      | None -> LocalAssum (i,t')
@@ -145,7 +145,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let assums = List.filter is_local_assum newps in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
   let ty = Inductive (params,(finite != Declarations.BiFinite)) in
-  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
+  let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in
   let env2,sigma,impls,newfs,data =
     interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
   in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 89fd2b641..6b7746db4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1025,7 +1025,9 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
   let sr = smart_global reference in
   let inf_names =
     let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
-    Impargs.compute_implicits_names (Global.env ()) ty
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Impargs.compute_implicits_names env sigma (EConstr.of_constr ty)
   in
   let prev_names =
     try Arguments_renaming.arguments_names sr with Not_found -> inf_names
@@ -1253,7 +1255,7 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
@@ -1627,6 +1629,7 @@ let vernac_global_check c =
   let senv = Global.safe_env() in
   let uctx = UState.context_set uctx in
   let senv = Safe_typing.push_context_set false uctx senv in
+  let c = EConstr.to_constr sigma c in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
   print_safe_judgment env sigma j ++
@@ -1747,10 +1750,10 @@ let interp_search_restriction = function
 
 open Search
 
-let interp_search_about_item env =
+let interp_search_about_item env sigma =
   function
   | SearchSubPattern pat ->
-      let _,pat = intern_constr_pattern env pat in
+      let _,pat = intern_constr_pattern env sigma pat in
       GlobSearchSubPattern pat
   | SearchString (s,None) when Id.is_valid s ->
       GlobSearchString s
@@ -1796,13 +1799,13 @@ let vernac_search ~atts s gopt r =
     (* if goal selector is given and wrong, then let exceptions be raised. *)
     | Some g -> snd (Pfedit.get_goal_context g) , Some g
   in
-  let get_pattern c = snd (intern_constr_pattern env c) in
+  let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in
   let pr_search ref env c =
     let pr = pr_global ref in
     let pp = if !search_output_name_only
       then pr
       else begin
-        let pc = pr_lconstr_env env Evd.empty c in
+        let pc = pr_lconstr_env env Evd.(from_env env) c in
         hov 2 (pr ++ str":" ++ spc () ++ pc)
       end
     in Feedback.msg_notice pp
@@ -1815,7 +1818,8 @@ let vernac_search ~atts s gopt r =
   | SearchHead c ->
       (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchAbout sl ->
-      (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search
+      (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+       Search.prioritize_search) pr_search
 
 let vernac_locate = function
   | LocateAny (AN qid)  -> print_located_qualid qid
@@ -1910,8 +1914,7 @@ let vernac_check_guard () =
   let message =
     try
       let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in
-      Inductiveops.control_only_guard (Goal.V82.env sigma gl)
-	(EConstr.Unsafe.to_constr pfterm);
+      Inductiveops.control_only_guard (Goal.V82.env sigma gl) sigma pfterm;
       (str "The condition holds up to here")
     with UserError(_,s) ->
       (str ("Condition violated: ") ++s)