[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/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 *)