4 files changed, 38 insertions, 14 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 401ba0fba4..56f846ebdb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -68,10 +68,11 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   let inst = instance_of_univ_entry univs in
   (gr,inst)
 
-let interp_assumption ~program_mode sigma env impls c =
+let interp_assumption ~program_mode env sigma impl_env bl c =
   let flags = { Pretyping.all_no_fail_flags with program_mode } in
-  let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in
-  sigma, (ty, impls)
+  let sigma, (impls, ((env_bl, ctx), impls1)) = interp_context_evars ~program_mode ~impl_env env sigma bl in
+  let sigma, (ty, impls2) = interp_type_evars_impls ~flags env sigma ~impls c in
+  sigma, ty, impls1@impls2
 
 (* When monomorphic the universe constraints and universe names are
    declared with the first declaration only. *)
@@ -153,7 +154,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
   in
   (* We interpret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
-    let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
+    let sigma,t,imps = interp_assumption ~program_mode env sigma ienv [] c in
     let r = Retyping.relevance_of_type env sigma t in
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 3d425ad768..64b8212b90 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -14,6 +14,15 @@ open Constrexpr
 
 (** {6 Parameters/Assumptions} *)
 
+val interp_assumption
+  : program_mode:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> Constrintern.internalization_env
+  -> Constrexpr.local_binder_expr list
+  -> constr_expr
+  -> Evd.evar_map * EConstr.t * Impargs.manual_implicits
+
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 37b7106856..c1dbf0a1ea 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -81,14 +81,11 @@ let protect_pattern_in_binder bl c ctypopt =
   else
     (bl, c, ctypopt, fun f env evd c -> f env evd c)
 
-let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
+let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
-  let env = Global.env() in
-  (* Explicitly bound universes and constraints *)
-  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in
   (* Build the parameters *)
-  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
+  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode ~impl_env env evd bl in
   (* Build the type *)
   let evd, tyopt = Option.fold_left_map
       (interp_type_evars_impls ~flags ~impls env_bl)
@@ -111,12 +108,15 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   (* Declare the definition *)
   let c = EConstr.it_mkLambda_or_LetIn c ctx in
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
-  (c, tyopt), evd, udecl, imps
+  evd, (c, tyopt), imps
 
 let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = false in
-  let (body, types), evd, udecl, impargs =
-    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, (body, types), impargs =
+    interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
@@ -127,8 +127,11 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
 
 let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = true in
-  let (body, types), evd, udecl, impargs =
-    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, (body, types), impargs =
+    interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index d95e64a85f..7420235449 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -14,6 +14,17 @@ open Constrexpr
 
 (** {6 Definitions/Let} *)
 
+val interp_definition
+  :  program_mode:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> Constrintern.internalization_env
+  -> Constrexpr.local_binder_expr list
+  -> red_expr option
+  -> constr_expr
+  -> constr_expr option
+  -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits
+
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t