diff options
| -rw-r--r-- | library/lib.ml | 13 | ||||
| -rw-r--r-- | library/lib.mli | 3 | ||||
| -rw-r--r-- | toplevel/classes.ml | 11 | ||||
| -rw-r--r-- | toplevel/classes.mli | 4 | ||||
| -rw-r--r-- | toplevel/command.ml | 11 | ||||
| -rw-r--r-- | toplevel/command.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
7 files changed, 36 insertions, 21 deletions
diff --git a/library/lib.ml b/library/lib.ml index ac100b831..907d251e7 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -365,18 +365,21 @@ let end_compilation dir = (* Returns true if we are inside an opened module or module type *) -let is_module_gen which = +let is_module_gen which check = let test = function | _, OpenedModule (ty,_,_,_) -> which ty | _ -> false in try - let _ = find_entry_p test in true + match find_entry_p test with + | _, OpenedModule (ty,_,_,_) -> check ty + | _ -> assert false with Not_found -> false -let is_module_or_modtype () = is_module_gen (fun _ -> true) -let is_modtype () = is_module_gen (fun b -> b) -let is_module () = is_module_gen (fun b -> not b) +let is_module_or_modtype () = is_module_gen (fun _ -> true) (fun _ -> true) +let is_modtype () = is_module_gen (fun b -> b) (fun _ -> true) +let is_modtype_strict () = is_module_gen (fun _ -> true) (fun b -> b) +let is_module () = is_module_gen (fun b -> not b) (fun _ -> true) (* Returns the opening node of a given name *) let find_opening_node id = diff --git a/library/lib.mli b/library/lib.mli index eca3164e3..25c0e1b24 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -91,6 +91,9 @@ val sections_depth : unit -> int (** Are we inside an opened module type *) val is_module_or_modtype : unit -> bool val is_modtype : unit -> bool +(* [is_modtype_strict] checks not only if we are in a module type, but + if the latest module started is a module type. *) +val is_modtype_strict : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 49640ec4b..b3f9d4872 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -332,22 +332,23 @@ let context l = let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in - let fn (id, _, t) = + let fn status (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then let cst = Declare.declare_constant ~internal:Declare.KernelSilent id (ParameterEntry (None,t,None), IsAssumption Logical) in match class_of_constr t with | Some (rels, (tc, args) as _cl) -> - add_instance (Typeclasses.new_instance tc None false (ConstRef cst)) + add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); + status (* declare_subclasses (ConstRef cst) cl *) - | None -> () + | None -> status else ( let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) None (* inline *) (Loc.ghost, id)) - in List.iter fn (List.rev ctx) + [] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status) + in List.fold_left fn true (List.rev ctx) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index d628760db..cfb8362f0 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -67,7 +67,9 @@ val id_of_class : typeclass -> identifier (** Context command *) -val context : local_binder list -> unit +(** returns [false] if, for lack of section, it declares an assumption + (unless in a module type). *) +val context : local_binder list -> bool (** Forward ref for refine *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 8fd8fe116..3c85868d5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -160,7 +160,7 @@ let do_definition ident k bl red_option c ctypopt hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = - let r = match local with + let r,status = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident @@ -170,7 +170,7 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals"); let r = VarRef ident in - Typeclasses.declare_instance None true r; r + Typeclasses.declare_instance None true r; r,true | (Global|Local) -> let kn = declare_constant ident @@ -183,9 +183,10 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = strbrk " because it is at a global level"); Autoinstance.search_declaration (ConstRef kn); Typeclasses.declare_instance None false gr; - gr + gr , (Lib.is_modtype_strict ()) in - if is_coe then Class.try_add_new_coercion r local + if is_coe then Class.try_add_new_coercion r local; + status let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook @@ -197,7 +198,7 @@ let interp_assumption bl c = let declare_assumptions idl is_coe k c imps impl_is_on nl = !declare_assumptions_hook c; - List.iter (declare_assumption is_coe k c imps impl_is_on nl) idl + List.fold_left (fun status id -> declare_assumption is_coe k c imps impl_is_on nl id && status) true idl (* 3a| Elimination schemes for mutual inductive definitions *) diff --git a/toplevel/command.mli b/toplevel/command.mli index c7a23711c..47e6f5a25 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -47,13 +47,15 @@ val do_definition : identifier -> definition_kind -> val interp_assumption : local_binder list -> constr_expr -> types * Impargs.manual_implicits +(** returns [false] if the assumption is neither local to a section, + nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool (** implicit *) -> Entries.inline -> variable Loc.located -> unit + bool (** implicit *) -> Entries.inline -> variable Loc.located -> bool val declare_assumptions : variable Loc.located list -> coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool -> Entries.inline -> unit + bool -> Entries.inline -> bool (** {6 Inductive and coinductive types} *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2235dd880..c30c6c0c1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -509,13 +509,16 @@ let vernac_exact_proof c = let vernac_assumption kind l nl= let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> + let status = + List.fold_left (fun status (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; let t,imps = interp_assumption [] c in - declare_assumptions idl is_coe kind t imps false nl) l + declare_assumptions idl is_coe kind t imps false nl && status) true l + in + if not status then raise UnsafeSuccess let vernac_record k finite infer struc binders sort nameopt cfs = let const = match nameopt with @@ -774,7 +777,7 @@ let vernac_instance abst glob sup inst props pri = ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = - Classes.context l + if not (Classes.context l) then raise UnsafeSuccess let vernac_declare_instances glob ids = List.iter (fun (id) -> Classes.existing_instance glob id) ids |