From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- kernel/cbytecodes.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/cbytegen.ml | 4 +- kernel/cemitcodes.ml | 2 +- kernel/closure.ml | 4 +- kernel/closure.mli | 2 +- kernel/constr.ml | 2 +- kernel/constr.mli | 2 +- kernel/context.ml | 2 +- kernel/context.mli | 2 +- kernel/conv_oracle.ml | 2 +- kernel/conv_oracle.mli | 2 +- kernel/cooking.ml | 2 +- kernel/cooking.mli | 2 +- kernel/csymtable.ml | 2 +- kernel/csymtable.mli | 2 +- kernel/declarations.mli | 25 ++++++--- kernel/declareops.ml | 2 +- kernel/declareops.mli | 2 +- kernel/entries.mli | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 2 +- kernel/esubst.ml | 2 +- kernel/esubst.mli | 2 +- kernel/evar.ml | 2 +- kernel/evar.mli | 2 +- kernel/fast_typeops.ml | 8 +-- kernel/fast_typeops.mli | 2 +- kernel/indtypes.ml | 73 +++++++++++++++++--------- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 2 +- kernel/inductive.mli | 2 +- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 2 +- kernel/mod_typing.ml | 130 +++++++++++++++++++++++++--------------------- kernel/mod_typing.mli | 26 +++++++--- kernel/modops.ml | 9 ++-- kernel/modops.mli | 7 +-- kernel/names.ml | 2 +- kernel/names.mli | 12 ++--- kernel/nativecode.ml | 2 +- kernel/nativecode.mli | 2 +- kernel/nativeconv.ml | 2 +- kernel/nativeconv.mli | 2 +- kernel/nativeinstr.mli | 2 +- kernel/nativelambda.ml | 2 +- kernel/nativelambda.mli | 2 +- kernel/nativelib.ml | 14 ++++- kernel/nativelib.mli | 2 +- kernel/nativelibrary.ml | 2 +- kernel/nativelibrary.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/nativevalues.mli | 2 +- kernel/opaqueproof.ml | 2 +- kernel/opaqueproof.mli | 6 +-- kernel/pre_env.ml | 2 +- kernel/pre_env.mli | 2 +- kernel/primitives.ml | 2 +- kernel/primitives.mli | 2 +- kernel/reduction.ml | 4 +- kernel/reduction.mli | 2 +- kernel/retroknowledge.ml | 2 +- kernel/retroknowledge.mli | 2 +- kernel/safe_typing.ml | 4 +- kernel/safe_typing.mli | 2 +- kernel/sorts.ml | 2 +- kernel/sorts.mli | 2 +- kernel/subtyping.ml | 2 +- kernel/subtyping.mli | 2 +- kernel/term.ml | 2 +- kernel/term.mli | 2 +- kernel/term_typing.ml | 15 ++++-- kernel/term_typing.mli | 2 +- kernel/type_errors.ml | 2 +- kernel/type_errors.mli | 2 +- kernel/typeops.ml | 2 +- kernel/typeops.mli | 2 +- kernel/univ.ml | 12 +++-- kernel/univ.mli | 2 +- kernel/vars.ml | 2 +- kernel/vars.mli | 4 +- kernel/vconv.mli | 2 +- kernel/vm.ml | 2 +- kernel/vm.mli | 3 ++ 84 files changed, 285 insertions(+), 207 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 0a24a75d..f9cf2691 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* {utj_val = c; utj_type = s } @@ -52,8 +52,8 @@ let assumption_of_judgment env t ty = error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 90d9c55f..05d52b2d 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (* type without constructors *) true | _ -> false -let infos_and_sort env ctx t = - let rec aux env ctx t max = +let infos_and_sort env t = + let rec aux env t max = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in let env1 = Environ.push_rel (name,None,varj.utj_val) env in let max = Universe.sup max (univ_of_sort varj.utj_type) in - aux env1 ctx c2 max + aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max - in aux env ctx t Universe.type0m + in aux env t Universe.type0m (* Computing the levels of polymorphic inductive types @@ -148,14 +148,14 @@ let infos_and_sort env ctx t = (* This (re)computes informations relevant to extraction and the sort of an arity or type constructor; we do not to recompute universes constraints *) -let infer_constructor_packet env_ar_par ctx params lc = +let infer_constructor_packet env_ar_par params lc = (* type-check the constructors *) let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) - let levels = List.map (infos_and_sort env_ar_par ctx) lc in + let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in let level = List.fold_left (fun max l -> Universe.sup max l) min levels in @@ -261,8 +261,7 @@ let typecheck_inductive env mie = List.fold_right2 (fun ind arity_data inds -> let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par ContextSet.empty - params ind.mind_entry_lc in + infer_constructor_packet env_ar_par params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,lc',cstrs_univ) in ind'::inds) @@ -337,7 +336,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor + | LocalNotConstructor of rel_context * constr list | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -348,7 +347,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c err = let (lpar,c') = mind_extract_params nbpar c in match err with | LocalNonPos kt -> @@ -356,9 +355,11 @@ let explain_ind_err id ntyp env nbpar c nargs err = | LocalNotEnoughArgs kt -> raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor -> + | LocalNotConstructor (paramsctxt,args)-> + let nparams = rel_context_nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, + List.length args - nparams))) | LocalNonPar (n,i,l) -> raise (InductiveError (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) @@ -547,7 +548,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> check_correct_par ienv hyps (ntypes - i) largs - | _ -> raise (IllFormedInd LocalNotConstructor) + | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs))) end else if not (List.for_all (noccur_between n ntypes) largs) @@ -563,7 +564,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname try check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err id (ntypes-i) env lparams c nargs err) + explain_ind_err id (ntypes-i) env lparams c err) (Array.of_list lcnames) indlc in let irecargs = Array.map snd irecargs_nmr @@ -652,14 +653,13 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = - let subst, inst = + let _, _, subst, inst = List.fold_right - (fun (na, b, t) (subst, inst) -> + (fun (na, b, t) (i, j, subst, inst) -> match b with - | None -> (mkRel 1 :: List.map (lift 1) subst, - mkRel 1 :: List.map (lift 1) inst) - | Some b -> (substl subst b) :: subst, List.map (lift 1) inst) - paramslet ([], []) + | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst) + | Some b -> (i, j-1, substl subst b :: subst, inst)) + paramslet (nparamargs, List.length paramslet, [], []) in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst @@ -689,14 +689,37 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with - | Some c -> (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: subst) + | Some c -> + (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) + let c = liftn 1 j c in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) + let c2 = substl letsubst c in + (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] + to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) + let letsubst = c2 :: letsubst in + (i, j+1, kns, pbs, subst, letsubst) | None -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in - let projty = substl letsubst (liftn 1 j t) in - let ty = substl subst (liftn 1 j t) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + let projty = substl letsubst t in + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst t in let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in let compat = compat_body ty (j - 1) in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 01acdce5..a7bf8fab 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* mp @@ -183,8 +183,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = begin try let mtb_old = module_type_of_module old in - Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints - with Failure _ -> error_incorrect_with_constraint lab + let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in + Univ.ContextSet.add_constraints chk_cst old.mod_constraints + with Failure _ -> + (* TODO: where can a Failure come from ??? *) + error_incorrect_with_constraint lab end | Algebraic (NoFunctor (MEident(mp'))) -> check_modpath_equiv env' mp1 mp'; @@ -238,104 +241,89 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Not_found -> error_no_such_label lab | Reduction.NotConvertible -> error_incorrect_with_constraint lab -let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg - let check_with env mp (sign,alg,reso,cst) = function |WithDef(idl,c) -> let struc = destr_nofunctor sign in let struc',c',cst' = check_with_def env struc (idl,c) mp reso in - let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in - (NoFunctor struc'),alg',reso, cst+++cst' + let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in + NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst' |WithMod(idl,mp1) as wd -> let struc = destr_nofunctor sign in let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in - let alg' = mk_alg_with alg wd in - (NoFunctor struc'),alg',reso', cst+++cst' + NoFunctor struc', MEwith (alg,wd), reso', cst+++cst' -let mk_alg_app mpo alg arg = match mpo, alg with - | Some _, Some alg -> Some (MEapply (alg,arg)) - | _ -> None +let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = + let farg_id, farg_b, fbody_b = destr_functor sign in + let mtb = module_type_of_module (lookup_module mp1 env) in + let cst2 = Subtyping.check_subtypes env mtb farg_b in + let mp_delta = discr_resolver mtb in + let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in + let subst = map_mbid farg_id mp1 mp_delta in + let body = subst_signature subst fbody_b in + let alg' = mkalg alg mp1 in + let reso' = subst_codom_delta_resolver subst reso in + body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1 (** Translation of a module struct entry : - We translate to a module when a [module_path] is given, otherwise to a module type. - The first output is the expanded signature - The second output is the algebraic expression, kept for the extraction. - It is never None when translating to a module, but for module type - it could not be contain [SEBapply] or [SEBfunctor]. *) +let mk_alg_app alg arg = MEapply (alg,arg) + let rec translate_mse env mpo inl = function - |MEident mp1 -> - let sign,reso = match mpo with - |Some mp -> - let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in - mb.mod_type, mb.mod_delta - |None -> - let mtb = lookup_modtype mp1 env in - mtb.mod_type, mtb.mod_delta + |MEident mp1 as me -> + let mb = match mpo with + |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false + |None -> lookup_modtype mp1 env in - sign,Some (MEident mp1),reso,Univ.ContextSet.empty + mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty |MEapply (fe,mp1) -> - translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo) + translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app |MEwith(me, with_decl) -> assert (mpo == None); (* No 'with' syntax for modules *) let mp = mp_from_mexpr me in check_with env mp (translate_mse env None inl me) with_decl -and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = - let farg_id, farg_b, fbody_b = destr_functor sign in - let mtb = module_type_of_module (lookup_module mp1 env) in - let cst2 = Subtyping.check_subtypes env mtb farg_b in - let mp_delta = discr_resolver mtb in - let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in - let subst = map_mbid farg_id mp1 mp_delta in - let body = subst_signature subst fbody_b in - let alg' = mkalg alg mp1 in - let reso' = subst_codom_delta_resolver subst reso in - body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1 - -let mk_alg_funct mpo mbid mtb alg = match mpo, alg with - | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg)) - | _ -> None - -let mk_mod mp e ty ty' cst reso = +let mk_mod mp e ty cst reso = { mod_mp = mp; mod_expr = e; mod_type = ty; - mod_type_alg = ty'; + mod_type_alg = None; mod_constraints = cst; mod_delta = reso; mod_retroknowledge = [] } -let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso +let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso let rec translate_mse_funct env mpo inl mse = function |[] -> let sign,alg,reso,cst = translate_mse env mpo inl mse in - sign, Option.map (fun a -> NoFunctor a) alg, reso, cst + sign, NoFunctor alg, reso, cst |(mbid, ty) :: params -> let mp_id = MPbound mbid in let mtb = translate_modtype env mp_id inl ([],ty) in let env' = add_module_type mp_id mtb env in let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in - let alg' = mk_alg_funct mpo mbid mtb alg in + let alg' = MoreFunctor (mbid,mtb,alg) in MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints and translate_modtype env mp inl (params,mte) = let sign,alg,reso,cst = translate_mse_funct env None inl mte params in let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in let mtb' = subst_modtype_and_resolver mtb mp in - { mtb' with mod_type_alg = alg } + { mtb' with mod_type_alg = Some alg } (** [finalize_module] : - from an already-translated (or interactive) implementation - and a signature entry, produce a final [module_expr] *) + from an already-translated (or interactive) implementation and + an (optional) signature entry, produces a final [module_body] *) let finalize_module env mp (sign,alg,reso,cst) restype = match restype with |None -> let impl = match alg with Some e -> Algebraic e | None -> FullStruct in - mk_mod mp impl sign None cst reso + mk_mod mp impl sign cst reso |Some (params_mte,inl) -> let res_mtb = translate_modtype env mp inl params_mte in let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in @@ -344,33 +332,59 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; - (** cst from module body typing, cst' from subtyping, - and constraints from module type. *) - mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) } + (** cst from module body typing, + cst' from subtyping, + constraints from module type. *) + mod_constraints = + Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) } let translate_module env mp inl = function |MType (params,ty) -> let mtb = translate_modtype env mp inl (params,ty) in module_body_of_type mp mtb |MExpr (params,mse,oty) -> - let t = translate_mse_funct env (Some mp) inl mse params in + let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in let restype = Option.map (fun ty -> ((params,ty),inl)) oty in - finalize_module env mp t restype + finalize_module env mp (sg,Some alg,reso,cst) restype + +(** We now forbid any Include of functors with restricted signatures. + Otherwise, we could end with the creation of undesired axioms + (see #3746). Note that restricted non-functorized modules are ok, + thanks to strengthening. *) + +let rec unfunct = function + |NoFunctor me -> me + |MoreFunctor(_,_,me) -> unfunct me + +let rec forbid_incl_signed_functor env = function + |MEapply(fe,_) -> forbid_incl_signed_functor env fe + |MEwith _ -> assert false (* No 'with' syntax for modules *) + |MEident mp1 -> + let mb = lookup_module mp1 env in + match mb.mod_type, mb.mod_type_alg, mb.mod_expr with + |MoreFunctor _, Some _, _ -> + (* functor + restricted signature = error *) + error_include_restricted_functor mp1 + |MoreFunctor _, None, Algebraic me -> + (* functor, no signature yet, a definition which may be restricted *) + forbid_incl_signed_functor env (unfunct me) + |_ -> () let rec translate_mse_inclmod env mp inl = function |MEident mp1 -> let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in let sign = clean_bounded_mod_expr mb.mod_type in - sign,None,mb.mod_delta,Univ.ContextSet.empty + sign,(),mb.mod_delta,Univ.ContextSet.empty |MEapply (fe,arg) -> let ftrans = translate_mse_inclmod env mp inl fe in - translate_apply env inl ftrans arg (fun _ _ -> None) + translate_apply env inl ftrans arg (fun _ _ -> ()) |MEwith _ -> assert false (* No 'with' syntax for modules *) let translate_mse_incl is_mod env mp inl me = if is_mod then + let () = forbid_incl_signed_functor env me in translate_mse_inclmod env mp inl me else let mtb = translate_modtype env mp inl ([],me) in let sign = clean_bounded_mod_expr mtb.mod_type in - sign,None,mtb.mod_delta,mtb.mod_constraints + sign,(),mtb.mod_delta,mtb.mod_constraints diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index bc0e2020..5949dad0 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_path -> inline -> module_entry -> module_body +(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] + cannot be [None] (and of course [mod_expr] is [Abstract]). *) + val translate_modtype : env -> module_path -> inline -> module_type_entry -> module_type_body @@ -24,20 +33,21 @@ val translate_modtype : - We translate to a module when a [module_path] is given, otherwise to a module type. - The first output is the expanded signature - - The second output is the algebraic expression, kept for the extraction. - It is never None when translating to a module, but for module type - it could not be contain applications or functors. -*) + - The second output is the algebraic expression, kept mostly for + the extraction. *) type 'alg translation = - module_signature * 'alg option * delta_resolver * Univ.ContextSet.t + module_signature * 'alg * delta_resolver * Univ.ContextSet.t val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** From an already-translated (or interactive) implementation and + an (optional) signature entry, produces a final [module_body] *) + val finalize_module : - env -> module_path -> module_expression translation -> + env -> module_path -> (module_expression option) translation -> (module_type_entry * inline) option -> module_body @@ -46,4 +56,4 @@ val finalize_module : val translate_mse_incl : bool -> env -> module_path -> inline -> module_struct_entry -> - module_alg_expr translation + unit translation diff --git a/kernel/modops.ml b/kernel/modops.ml index cbb79633..6fe7e382 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a -val error_application_to_not_path : module_struct_entry -> 'a - val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a @@ -152,3 +151,5 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a + +val error_include_restricted_functor : module_path -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b63..f5d954e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ModPath.t val constr_modpath : constructor -> ModPath.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 98b2d6d2..9d181b47 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* true + | Unix.WEXITED n -> + Pp.(msg_warning (str "command exited with status " ++ int n)); false + | Unix.WSIGNALED n -> + Pp.(msg_warning (str "command killed by signal " ++ int n)); false + | Unix.WSTOPPED n -> + Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in + res, link_filename with Unix.Unix_error (e,_,_) -> Pp.(msg_warning (str (Unix.error_message e))); false, link_filename diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 0941dc56..12ad3cf2 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0df26d62..9a83ca70 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - Environ.add_constant kn cb env + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + Environ.push_context ~strict:true cb.const_universes env + else env | kn, cb, `Opaque(_, ctx), _ -> - let env = Environ.add_constant kn cb env in - Environ.push_context_set - ~strict:(not cb.const_polymorphic) ctx env in + let env = Environ.add_constant kn cb env in + if not cb.const_polymorphic then + let env = Environ.push_context ~strict:true cb.const_universes env in + Environ.push_context_set ~strict:true ctx env + else env in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 2e6aa161..fcd95576 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* not (Level.is_prop x)) a); + a let to_array a = a @@ -1715,7 +1717,7 @@ struct let subst_fn fn t = let t' = CArray.smartmap fn t in - if t' == t then t else t' + if t' == t then t else of_array t' let levels x = LSet.of_array x @@ -2030,8 +2032,8 @@ let dump_universes output g = let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> let u_str = Level.to_string u in - List.iter (fun v -> output Lt (Level.to_string v) u_str) lt; - List.iter (fun v -> output Le (Level.to_string v) u_str) le + List.iter (fun v -> output Lt u_str (Level.to_string v)) lt; + List.iter (fun v -> output Le u_str (Level.to_string v)) le | Equiv v -> output Eq (Level.to_string u) (Level.to_string v) in diff --git a/kernel/univ.mli b/kernel/univ.mli index c926c57b..9788f129 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> constr if two names are identical, the one of least indice is kept *) val subst_vars : Id.t list -> constr -> constr -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] +(** [substn_vars n [id1;...;idk] t] substitute [VAR idj] by [Rel j+n-1] in [t] if two names are identical, the one of least indice is kept *) val substn_vars : int -> Id.t list -> constr -> constr diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 49e5d23e..7e5397c0 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds val pr_whd : whd -> Pp.std_ppcmds +val pr_stack : stack -> Pp.std_ppcmds (** Constructors *) -- cgit v1.2.3