diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/classes.ml | 24 | ||||
-rw-r--r-- | toplevel/command.ml | 4 | ||||
-rw-r--r-- | toplevel/command.mli | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 27 insertions, 7 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 2d5cd659f..2df66180c 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -257,6 +257,14 @@ let named_of_rel_context l = l ([], []) in ctx +let push_named_context = List.fold_right push_named + +let rec list_filter_map f = function + | [] -> [] + | hd :: tl -> match f hd with + | None -> list_filter_map f tl + | Some x -> x :: list_filter_map f tl + let context ?(hook=fun _ -> ()) l = let env = Global.env() in let evars = ref Evd.empty in @@ -267,6 +275,14 @@ let context ?(hook=fun _ -> ()) l = let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in + let env = push_named_context ctx env in + let keeps = + List.fold_left (fun acc (id,_,t) -> + match class_of_constr t with + | None -> acc + | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc) + [] ctx + in List.iter (function (id,_,t) -> if Lib.is_modtype () then let cst = Declare.declare_internal_constant id @@ -278,10 +294,14 @@ let context ?(hook=fun _ -> ()) l = hook (ConstRef cst) | None -> () else ( - let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + let impl = List.exists (fun (x,_) -> + match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + and keep = + let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in + List.concat l in Command.declare_one_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); + [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id); match class_of_constr t with | None -> () | Some tc -> hook (VarRef id))) diff --git a/toplevel/command.ml b/toplevel/command.ml index 820e0f156..d2eed98e4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1102,9 +1102,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = | None -> (match local with | Local -> - let impl=false and keep=false in (* copy values from Vernacentries *) + let impl=false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl,keep) in + let c = SectionLocalAssum (t_i,impl,[]) in let _ = declare_variable id (Lib.cwd(),c,k) in (Local,VarRef id,imps) | Global -> diff --git a/toplevel/command.mli b/toplevel/command.mli index 73d8516f0..d5283a6db 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr -> val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> Impargs.manual_explicitation list -> - bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit + bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located -> unit val set_declare_assumption_hook : (types -> unit) -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> - bool -> bool -> bool -> unit + bool -> identifier list -> bool -> unit val open_temp_scopes : Topconstr.scope_name option -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 90e211d03..5d76f4ff2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -373,7 +373,7 @@ let vernac_assumption kind l nl= List.iter (fun lid -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; - declare_assumption idl is_coe kind [] c false false nl) l + declare_assumption idl is_coe kind [] c false [] nl) l let vernac_record k finite infer struc binders sort nameopt cfs = let const = match nameopt with |