diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 13 | ||||
| -rw-r--r-- | toplevel/command.ml | 10 | ||||
| -rw-r--r-- | toplevel/command.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 9 insertions, 20 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 91bf5cd21..2eeb8a7de 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -275,14 +275,6 @@ 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 @@ -296,12 +288,9 @@ let context ?(hook=fun _ -> ()) l = else ( 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 *) keep (* always kept *) false (* inline *) (dummy_loc, id); + [] impl (* implicit *) 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 80de34458..1da86712d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -169,12 +169,12 @@ let syntax_definition ident (vars,c) local onlyparse = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident - (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in + (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ @@ -196,13 +196,13 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let declare_assumption_hook = ref ignore let set_declare_assumption_hook = (:=) declare_assumption_hook -let declare_assumption idl is_coe k bl c impl keep nl = +let declare_assumption idl is_coe k bl c impl nl = if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in let env = Global.env () in let c', imps = interp_type_evars_impls env c in !declare_assumption_hook c'; - List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl + List.iter (declare_one_assumption is_coe k c' imps impl nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -1106,7 +1106,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = | Local -> let impl=false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl,[]) 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 d5283a6db..d648fc10e 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 *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located -> unit + bool (* implicit *) -> 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 -> identifier list -> bool -> unit + bool -> bool -> unit val open_temp_scopes : Topconstr.scope_name option -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 887d5a616..be7c29bab 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 [] 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 |