diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 7301e1fff7..73d0be04df 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -84,8 +84,8 @@ match local with in (gr,inst,Lib.is_modtype_strict ()) -let interp_assumption sigma env impls c = - let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in +let interp_assumption ~program_mode sigma env impls c = + let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in sigma, (ty, impls) (* When monomorphic the universe constraints are declared with the first declaration only. *) @@ -131,7 +131,7 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions kind nl l = +let do_assumptions ~program_mode kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in @@ -147,7 +147,7 @@ let do_assumptions kind nl l = in (* We intepret 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 sigma env ienv c in + let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun {CAst.v=id} ienv -> |