[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.

4 files changed, 8 insertions, 10 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 275a079d5..33d674ff5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -643,8 +643,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 (* A function which checks that a term well typed verifies both
    syntactic conditions *)
 
-let control_only_guard env c =
-  let check_fix_cofix e c = match kind c with
+let control_only_guard env sigma c =
+  let check_fix_cofix e c =
+    match kind (EConstr.to_constr sigma c) with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
@@ -653,6 +654,6 @@ let control_only_guard env c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    iter_constr_with_full_binders push_rel iter env c
+    iter_constr_with_full_binders sigma EConstr.push_rel iter env c
   in
   iter env c
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 55149552a..8efa087a7 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -198,4 +198,4 @@ val type_of_inductive_knowing_conclusion :
   env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types
 
 (********************)
-val control_only_guard : env -> types -> unit
+val control_only_guard : env -> Evd.evar_map -> EConstr.types -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6700748eb..79d255b0b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1205,8 +1205,7 @@ let all_no_fail_flags = default_inference_flags false
 
 let ise_pretype_gen_ctx flags env sigma lvar kind c =
   let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in
-  let evd, f = Evarutil.nf_evars_and_universes evd in
-    f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd
+  c, Evd.evar_universe_context evd
 
 (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 864768fe5..ee568fbc4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -12,7 +12,6 @@
    into elementary ones, insertion of coercions and resolution of
    implicit arguments. *)
 
-open Constr
 open Environ
 open Evd
 open EConstr
@@ -26,7 +25,7 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
-  ?loc:Loc.t -> env -> int list list -> rec_declaration -> int array
+  ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
@@ -85,9 +84,8 @@ val understand_ltac : inference_flags ->
     heuristics (but no external tactic solver hook), as well as to
     ensure that conversion problems are all solved and that no
     unresolved evar remains, expanding evars. *)
-
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
-  env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context
+  env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
 
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver