[econstr] Continue consolidation of EConstr API under `interp`.

This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.

The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.

We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.

In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.

Also, the new return type of `Pretyping.understand` should undergo
careful review.

We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.

Some TODOs are:

- impargs was calling whd_all, the Econstr equivalent can be either
  + Reductionops.whd_all [which does refolding and no sharing]
  + Reductionops.clos_whd_flags with all as a flag.

1 files changed, 3 insertions, 5 deletions

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