Generalizing and exporting interp_assumption/interp_definition.

This shall be for Record fields consumption.

1 files changed, 5 insertions, 4 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