[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, 3 deletions

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 22ec6c5b1b..9a10fb805a 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -199,7 +199,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
     ltac_extra = extra;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
+    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c
   in
   (c',if !strict_check then None else Some c)
 
@@ -316,7 +316,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
     ltac_extra = ist.extra;
   } in
   let metas,pat = Constrintern.intern_constr_pattern
-    ist.genv ~as_type ~ltacvars pc
+    ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars pc
   in
   let (glob,_ as c) = intern_constr_gen true false ist pc in
   let bound_names = Glob_ops.bound_glob_vars glob in
@@ -335,7 +335,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p =
           ltac_bound = Id.Set.empty;
           ltac_extra = ist.extra;
         } in
-      Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p
+      Constrintern.intern_constr_pattern ist.genv Evd.(from_env ist.genv) ~as_type ~ltacvars p
     else
       [], dummy_pat in
   let (glob,_ as c) = intern_constr_gen true false ist p in