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

8 files changed, 152 insertions, 147 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d03aa3552..9053cdc24 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -184,14 +184,14 @@ let compute_explicitable_implicit imps = function
       (* Unable to know in advance what the implicit arguments will be *)
       []
 
-let compute_internalization_data env ty typ impl =
-  let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in
+let compute_internalization_data env sigma ty typ impl =
+  let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
   let expls_impl = compute_explicitable_implicit impl ty in
-  (ty, expls_impl, impl, compute_arguments_scope typ)
+  (ty, expls_impl, impl, compute_arguments_scope sigma typ)
 
-let compute_internalization_env env ?(impls=empty_internalization_env) ty =
+let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
   List.fold_left3
-    (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map)
+    (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map)
     impls
 
 (**********************************************************************)
@@ -2207,9 +2207,9 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Id.Set.empty
 
-let scope_of_type_kind = function
+let scope_of_type_kind sigma = function
   | IsType -> Notation.current_type_scope_name ()
-  | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ)
+  | OfType typ -> compute_type_scope sigma typ
   | WithoutTypeConstraint -> None
 
 let empty_ltac_sign = {
@@ -2218,19 +2218,17 @@ let empty_ltac_sign = {
   ltac_extra = Genintern.Store.empty;
 }
 
-let intern_gen kind env
+let intern_gen kind env sigma
                ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
                c =
-  let tmp_scope = scope_of_type_kind kind in
+  let tmp_scope = scope_of_type_kind sigma kind in
   internalize env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
     pattern_mode (ltacvars, Id.Map.empty) c
 
-let intern_constr env c = intern_gen WithoutTypeConstraint env c
-
-let intern_type env c = intern_gen IsType env c
-
+let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
+let intern_type env sigma c = intern_gen IsType env sigma c
 let intern_pattern globalenv patt =
   try
     intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
@@ -2245,7 +2243,7 @@ let intern_pattern globalenv patt =
 (* All evars resolved *)
 
 let interp_gen kind env sigma ?(impls=empty_internalization_env) c =
-  let c = intern_gen kind ~impls env c in
+  let c = intern_gen kind ~impls env sigma c in
   understand ~expected_type:kind env sigma c
 
 let interp_constr env sigma ?(impls=empty_internalization_env) c =
@@ -2260,13 +2258,13 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ =
 (* Not all evars expected to be resolved *)
 
 let interp_open_constr env sigma c =
-  understand_tcc env sigma (intern_constr env c)
+  understand_tcc env sigma (intern_constr env sigma c)
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
 let interp_constr_evars_gen_impls env sigma
     ?(impls=empty_internalization_env) expected_type c =
-  let c = intern_gen expected_type ~impls env c in
+  let c = intern_gen expected_type ~impls env sigma c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
   let sigma, c = understand_tcc env sigma ~expected_type c in
   sigma, (c, imps)
@@ -2283,7 +2281,7 @@ let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
 let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
-  let c = intern_gen expected_type ~impls env c in
+  let c = intern_gen expected_type ~impls env sigma c in
   understand_tcc env sigma ~expected_type c
 
 let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
@@ -2297,9 +2295,9 @@ let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
 
 (* Miscellaneous *)
 
-let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
+let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
-            ~pattern_mode:true ~ltacvars env c in
+            ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
@@ -2323,16 +2321,14 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
 (* Interpret binders and contexts  *)
 
 let interp_binder env sigma na t =
-  let t = intern_gen IsType env t in
+  let t = intern_gen IsType env sigma t in
   let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
   understand ~expected_type:IsType env sigma t'
 
-let interp_binder_evars env evdref na t =
-  let t = intern_gen IsType env t in
+let interp_binder_evars env sigma na t =
+  let t = intern_gen IsType env sigma t in
   let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
-  let evd, c = understand_tcc env !evdref ~expected_type:IsType t' in
-  evdref := evd;
-  c
+  understand_tcc env sigma ~expected_type:IsType t'
 
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 7411fb84b..563230b59 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) -> *)
diff --git a/interp/declare.ml b/interp/declare.ml
index dfa84f278..f6d7b45c3 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -135,7 +135,7 @@ let set_declare_scheme f = declare_scheme := f
 let update_tables c =
   declare_constant_implicits c;
   Heads.declare_head (EvalConstRef c);
-  Notation.declare_ref_arguments_scope (ConstRef c)
+  Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
 
 let register_side_effect (c, role) =
   let o = inConstant {
@@ -275,7 +275,7 @@ let inVariable : variable_obj -> obj =
 let declare_variable id obj =
   let oname = add_leaf id (inVariable (Inr (id,obj))) in
   declare_var_implicits id;
-  Notation.declare_ref_arguments_scope (VarRef id);
+  Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
   Heads.declare_head (EvalVarRef id);
   oname
 
@@ -283,9 +283,9 @@ let declare_variable id obj =
 
 let declare_inductive_argument_scopes kn mie =
   List.iteri (fun i {mind_entry_consnames=lc} ->
-    Notation.declare_ref_arguments_scope (IndRef (kn,i));
+    Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
     for j=1 to List.length lc do
-      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
+      Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j));
     done) mie.mind_entry_inds
 
 let inductive_names sp kn mie =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index ed1cd5276..6767af6d8 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -7,21 +7,20 @@
 (************************************************************************)
 
 open CErrors
+open Pp
 open Util
 open Names
-open Globnames
 open Constr
-open Reduction
+open Globnames
 open Declarations
-open Environ
-open Libobject
+open Decl_kinds
 open Lib
-open Pp
-open Constrexpr
+open Libobject
+open EConstr
 open Termops
+open Reductionops
+open Constrexpr
 open Namegen
-open Decl_kinds
-open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
@@ -165,8 +164,8 @@ let update pos rig (na,st) =
   in na, Some e
 
 (* modified is_rigid_reference with a truncated env *)
-let is_flexible_reference env bound depth f =
-  match kind f with
+let is_flexible_reference env sigma bound depth f =
+  match kind sigma f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
     | Rel n -> (* since local definitions have been expanded *) false
@@ -174,102 +173,101 @@ let is_flexible_reference env bound depth f =
         let cb = Environ.lookup_constant kn env in
 	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
-        env |> Environ.lookup_named id |> is_local_def
+        env |> Environ.lookup_named id |> NamedDecl.is_local_def
     | Ind _ | Construct _ -> false
     |  _ -> true
 
 let push_lift d (e,n) = (push_rel d e,n+1)
 
-let is_reversible_pattern bound depth f l =
-  isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) &&
-  Array.for_all (fun c -> isRel c && destRel c < depth) l &&
+let is_reversible_pattern sigma bound depth f l =
+  isRel sigma f && let n = destRel sigma f in (n < bound+depth) && (n >= depth) &&
+  Array.for_all (fun c -> isRel sigma c && destRel sigma c < depth) l &&
   Array.distinct l
 
 (* Precondition: rels in env are for inductive types only *)
-let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
+let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc =
   let rec frec rig (env,depth as ed) c =
-    let hd = if strict then whd_all env c else c in
+    let hd = if strict then whd_all env sigma c else c in
     let c = if strongly_strict then hd else c in
-    match kind hd with
+    match kind sigma hd with
     | Rel n when (n < bound+depth) && (n >= depth) ->
 	let i = bound + depth - n - 1 in
         acc.(i) <- update pos rig acc.(i)
-    | App (f,l) when revpat && is_reversible_pattern bound depth f l ->
-	let i = bound + depth - destRel f - 1 in
+    | App (f,l) when revpat && is_reversible_pattern sigma bound depth f l ->
+        let i = bound + depth - EConstr.destRel sigma f - 1 in
 	acc.(i) <- update pos rig acc.(i)
-    | App (f,_) when rig && is_flexible_reference env bound depth f ->
+    | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
-          iter_constr_with_full_binders push_lift (frec false) ed c
+          iter_constr_with_full_binders sigma push_lift (frec false) ed c
     | Proj (p,c) when rig ->
       if strict then () else
-        iter_constr_with_full_binders push_lift (frec false) ed c	  
+        iter_constr_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
 	if strict then () else
-          iter_constr_with_full_binders push_lift (frec false) ed c
+          iter_constr_with_full_binders sigma push_lift (frec false) ed c
     | Evar _ -> ()
     | _ ->
-        iter_constr_with_full_binders push_lift (frec rig) ed c
+        iter_constr_with_full_binders sigma push_lift (frec rig) ed c
   in
-  let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in
+  let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
   acc
 
-let rec is_rigid_head t = match kind t with
+let rec is_rigid_head sigma t = match kind sigma t with
   | Rel _ | Evar _ -> false
   | Ind _ | Const _ | Var _ | Sort _ -> true
-  | Case (_,_,f,_) -> is_rigid_head f
+  | Case (_,_,f,_) -> is_rigid_head sigma f
   | Proj (p,c) -> true
   | App (f,args) ->
-      (match kind f with
-	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
-	| _ -> is_rigid_head f)
+      (match kind sigma f with
+        | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
+        | _ -> is_rigid_head sigma f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
   | Prod _ | Meta _ | Cast _ -> assert false
 
 (* calcule la liste des arguments implicites *)
 
 let find_displayed_name_in all avoid na (env, b) =
-  let b = EConstr.of_constr b in
   let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
   if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
   else compute_displayed_name_in Evd.empty flag avoid na b
 
-let compute_implicits_gen strict strongly_strict revpat contextual all env t =
+let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) =
   let rigid = ref true in
   let open Context.Rel.Declaration in
-  let rec aux env avoid n names t =
-    let t = whd_all env t in
-    match kind t with
+  let rec aux env avoid n names (t : EConstr.t) =
+    let t = whd_all env sigma t in
+    match kind sigma t with
       | Prod (na,a,b) ->
 	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
-	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
+          add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1))
             (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
       | _ ->
-	  rigid := is_rigid_head t;
+          rigid := is_rigid_head sigma t;
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
 	  if contextual then
-	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
+            add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v
 	  else v
   in
-  match kind (whd_all env t) with
+  match kind sigma (whd_all env sigma t) with
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
 	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
 
-let compute_implicits_flags env f all t =
+let compute_implicits_flags env sigma f all t =
   compute_implicits_gen
     (f.strict || f.strongly_strict) f.strongly_strict
-    f.reversible_pattern f.contextual all env t
+    f.reversible_pattern f.contextual all env sigma t
 
-let compute_auto_implicits env flags enriching t =
-  if enriching then compute_implicits_flags env flags true t
-  else compute_implicits_gen false false false true true env t
+let compute_auto_implicits env sigma flags enriching t =
+  if enriching then compute_implicits_flags env sigma flags true t
+  else compute_implicits_gen false false false true true env sigma t
 
-let compute_implicits_names env t =
-  let _, impls = compute_implicits_gen false false false false true env t in
+let compute_implicits_names env sigma t =
+  let _, impls = compute_implicits_gen false false false false true env sigma t in
   List.map fst impls
 
 (* Extra information about implicit arguments *)
@@ -398,24 +396,25 @@ let set_manual_implicits env flags enriching autoimps l =
   in
   merge 1 l autoimps
 
-let compute_semi_auto_implicits env f manual t =
+let compute_semi_auto_implicits env sigma f manual t =
   match manual with
   | [] ->
       if not f.auto then [DefaultImpArgs, []]
-      else let _,l = compute_implicits_flags env f false t in
+      else let _,l = compute_implicits_flags env sigma f false t in
 	     [DefaultImpArgs, prepare_implicits f l]
   | _ ->
-      let _,autoimpls = compute_auto_implicits env f f.auto t in
+      let _,autoimpls = compute_auto_implicits env sigma f f.auto t in
       [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
 
 (*s Constants. *)
 
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
+  let sigma = Evd.from_env env in
   let cb = Environ.lookup_constant cst env in
-  let ty = cb.const_type in
-  let impls = compute_semi_auto_implicits env flags manual ty in
-    impls
+  let ty = of_constr cb.const_type in
+  let impls = compute_semi_auto_implicits env sigma flags manual ty in
+  impls
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -424,7 +423,8 @@ let compute_constant_implicits flags manual cst =
 
 let compute_mib_implicits flags manual kn =
   let env = Global.env () in
-  let mib = lookup_mind kn env in
+  let sigma = Evd.from_env env in
+  let mib = Environ.lookup_mind kn env in
   let ar =
     Array.to_list
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
@@ -433,14 +433,14 @@ let compute_mib_implicits flags manual kn =
 	  let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
 	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
-  let env_ar = push_rel_context ar env in
+  let env_ar = Environ.push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
     let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
-    ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
+    ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)),
      Array.mapi (fun j c ->
-       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
-       mip.mind_nf_lc)
+       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c))
+       (Array.map of_constr mip.mind_nf_lc))
   in
   Array.mapi imps_one_inductive mib.mind_packets
 
@@ -453,7 +453,8 @@ let compute_all_mib_implicits flags manual kn =
 
 let compute_var_implicits flags manual id =
   let env = Global.env () in
-  compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env))
+  let sigma = Evd.from_env env in
+  compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env))
 
 (* Implicits of a global reference. *)
 
@@ -524,7 +525,7 @@ let impls_of_context ctx =
   | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
   | _ -> None
   in
-  List.rev_map map (List.filter (fst %> is_local_assum) ctx)
+  List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx)
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
@@ -649,8 +650,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
 
 type manual_implicits = manual_explicitation list
 
-let compute_implicits_with_manual env typ enriching l =
-  let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in
+let compute_implicits_with_manual env sigma typ enriching l =
+  let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
   set_manual_implicits env !implicit_args enriching autoimpls l
 
 let check_inclusion l =
@@ -674,9 +675,10 @@ let projection_implicits env p impls =
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
-  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
+  let sigma = Evd.from_env env in
+  let t, _ = Global.type_of_global_in_context env ref in
   let enriching = Option.default flags.auto enriching in
-  let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
+  let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in
   let l' = match l with
     | [] -> assert false
     | [l] ->
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 40fa4cb26..dcfe527b0 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Constr
+open EConstr
 open Globnames
 open Environ
 
@@ -90,10 +90,10 @@ type manual_explicitation = Constrexpr.explicitation *
 
 type manual_implicits = manual_explicitation list
 
-val compute_implicits_with_manual : env -> types -> bool ->
+val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
   manual_implicits -> implicit_status list
 
-val compute_implicits_names : env -> types -> Name.t list
+val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list
 
 (** {6 Computation of implicits (done using the global environment). } *)
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index e631b3ea4..128152cc2 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,13 +61,16 @@ let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
   | CWith_Definition ((_,fqid),c) ->
-    let c, ectx = interp_constr env (Evd.from_env env) c in
+    let sigma = Evd.from_env env in
+    let c, ectx = interp_constr env sigma c in
     if Flags.is_universe_polymorphism () then
       let ctx = UState.context ectx in
       let inst, ctx = Univ.abstract_universes ctx in
-      let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+      let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+      let c = EConstr.to_constr sigma c in
       WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
     else
+      let c = EConstr.to_constr sigma c in
       WithDef (fqid,(c, None)), UState.context_set ectx
 
 let loc_of_module l = l.CAst.loc
diff --git a/interp/notation.ml b/interp/notation.ml
index ea7ef21b1..bf39c726a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -668,8 +668,8 @@ type scope_class = cl_typ
 let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
-let compute_scope_class t =
-  let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
+let compute_scope_class sigma t =
+  let (cl,_,_) = find_class_type sigma t in
   cl
 
 module ScopeClassOrd =
@@ -698,22 +698,22 @@ let find_scope_class_opt = function
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
-let rec compute_arguments_classes t =
-  match Constr.kind (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
+let rec compute_arguments_classes sigma t =
+  match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
     | Prod (_,t,u) ->
-	let cl = try Some (compute_scope_class t) with Not_found -> None in
-	cl :: compute_arguments_classes u
+        let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
+        cl :: compute_arguments_classes sigma u
     | _ -> []
 
-let compute_arguments_scope_full t =
-  let cls = compute_arguments_classes t in
+let compute_arguments_scope_full sigma t =
+  let cls = compute_arguments_classes sigma t in
   let scs = List.map find_scope_class_opt cls in
   scs, cls
 
-let compute_arguments_scope t = fst (compute_arguments_scope_full t)
+let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
 
-let compute_type_scope t =
-  find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
+let compute_type_scope sigma t =
+  find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
 
 let current_type_scope_name () =
    find_scope_class_opt (Some CL_SORT)
@@ -779,20 +779,24 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
 let classify_arguments_scope (req,_,_,_,_ as obj) =
   if req == ArgsScopeNoDischarge then Dispose else Substitute obj
 
-let rebuild_arguments_scope (req,r,n,l,_) =
+let rebuild_arguments_scope sigma (req,r,n,l,_) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-        let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in
-	(req,r,List.length scs,scs,cls)
+      let env = Global.env () in (*FIXME?*)
+      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let scs,cls = compute_arguments_scope_full sigma typ in
+      (req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
-	(* Add to the manually given scopes the one found automatically
-           for the extra parameters of the section. Discard the classes
-           of the manually given scopes to avoid further re-computations. *)
-        let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in
-	let l1 = List.firstn n l' in
-        let cls1 = List.firstn n cls in
-	(req,r,0,l1@l,cls1)
+      (* Add to the manually given scopes the one found automatically
+         for the extra parameters of the section. Discard the classes
+         of the manually given scopes to avoid further re-computations. *)
+      let env = Global.env () in (*FIXME?*)
+      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let l',cls = compute_arguments_scope_full sigma typ in
+      let l1 = List.firstn n l' in
+      let cls1 = List.firstn n cls in
+      (req,r,0,l1@l,cls1)
 
 type arguments_scope_obj =
     arguments_scope_discharge_request * global_reference *
@@ -807,7 +811,8 @@ let inArgumentsScope : arguments_scope_obj -> obj =
       subst_function = subst_arguments_scope;
       classify_function = classify_arguments_scope;
       discharge_function = discharge_arguments_scope;
-      rebuild_function = rebuild_arguments_scope }
+      (* XXX: Should we pass the sigma here or not, see @herbelin's comment in 6511 *)
+      rebuild_function = rebuild_arguments_scope Evd.empty }
 
 let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 
@@ -819,7 +824,7 @@ let declare_arguments_scope local r scl =
   (* We empty the list of argument classes to disable further scope
      re-computations and keep these manually given scopes. *)
   declare_arguments_scope_gen req r 0 (scl,[])
-                              
+
 let find_arguments_scope r =
   try
     let (scl,cls,stamp) = Refmap.find r !arguments_scope in
@@ -832,12 +837,12 @@ let find_arguments_scope r =
       scl'
   with Not_found -> []
 
-let declare_ref_arguments_scope ref =
-  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
-  let (scs,cls as o) = compute_arguments_scope_full t in
+let declare_ref_arguments_scope sigma ref =
+  let env = Global.env () in (* FIXME? *)
+  let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in
+  let (scs,cls as o) = compute_arguments_scope_full sigma typ in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
-
 (********************************)
 (* Encoding notations as string *)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index a4c79d6d3..79b56bd41 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -163,10 +163,10 @@ val subst_scope_class :
   Mod_subst.substitution -> scope_class -> scope_class option
 
 val declare_scope_class : scope_name -> scope_class -> unit
-val declare_ref_arguments_scope : global_reference -> unit
+val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit
 
-val compute_arguments_scope : Constr.types -> scope_name option list
-val compute_type_scope : Constr.types -> scope_name option
+val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
+val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
 
 (** Get the current scope bound to Sortclass, if it exists *)
 val current_type_scope_name : unit -> scope_name option