[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, 19 insertions, 20 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 7411fb84bb..563230b59a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -7,17 +7,17 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Evd
 open Environ
+open Misctypes
 open Libnames
 open Globnames
 open Glob_term
 open Pattern
+open EConstr
 open Constrexpr
 open Notation_term
 open Pretyping
-open Misctypes
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
@@ -58,10 +58,10 @@ type internalization_env = var_internalization_data Id.Map.t
 
 val empty_internalization_env : internalization_env
 
-val compute_internalization_data : env -> var_internalization_type ->
+val compute_internalization_data : env -> evar_map -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
-val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type ->
+val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
@@ -78,11 +78,10 @@ val empty_ltac_sign : ltac_sign
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
-val intern_constr : env -> constr_expr -> glob_constr
-
-val intern_type : env -> constr_expr -> glob_constr
+val intern_constr : env -> evar_map -> constr_expr -> glob_constr
+val intern_type : env -> evar_map -> constr_expr -> glob_constr
 
-val intern_gen : typing_constraint -> env ->
+val intern_gen : typing_constraint -> env -> evar_map ->
   ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
@@ -100,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
 
 val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
-  constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context
+  constr_expr -> types -> constr Evd.in_evar_universe_context
 
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
@@ -108,37 +107,37 @@ val interp_type : env -> evar_map -> ?impls:internalization_env ->
 (** Main interpretation function expecting all postponed problems to
     be resolved, but possibly leaving evars. *)
 
-val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
 val interp_constr_evars : env -> evar_map ->
-  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr
+  ?impls:internalization_env -> constr_expr -> evar_map * constr
 
 val interp_casted_constr_evars : env -> evar_map ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr
+  ?impls:internalization_env -> constr_expr -> types -> evar_map * constr
 
 val interp_type_evars : env -> evar_map ->
-  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types
+  ?impls:internalization_env -> constr_expr -> evar_map * types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
 val interp_constr_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  evar_map * (EConstr.constr * Impargs.manual_implicits)
+  evar_map * (constr * Impargs.manual_implicits)
 
 val interp_casted_constr_evars_impls : env -> evar_map ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types ->
-  evar_map * (EConstr.constr * Impargs.manual_implicits)
+  ?impls:internalization_env -> constr_expr -> types ->
+  evar_map * (constr * Impargs.manual_implicits)
 
 val interp_type_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  evar_map * (EConstr.types * Impargs.manual_implicits)
+  evar_map * (types * Impargs.manual_implicits)
 
 (** Interprets constr patterns *)
 
 val intern_constr_pattern :
-  env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+  env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
@@ -152,14 +151,14 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 val interp_binder  : env -> evar_map -> Name.t -> constr_expr -> 
   types Evd.in_evar_universe_context
 
-val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types
+val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * types
 
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map -> local_binder_expr list ->
-  evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits))
+  evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)