diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 10 | ||||
| -rw-r--r-- | library/declare.mli | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/library/declare.ml b/library/declare.ml index 56c789c1ed..9e94b150eb 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -389,20 +389,20 @@ let declare_projections mind = let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns - | Some None | None -> () + assert(eq_constant kn kn')) kns; true + | Some None | None -> false (* for initial declaration *) -let declare_mind isrecord mie = +let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - declare_projections mind; + let isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; - oname + oname, isprim (* Declaration messages *) diff --git a/library/declare.mli b/library/declare.mli index bda90229e6..5be8a5563f 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -67,8 +67,8 @@ val set_declare_scheme : (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of - the whole block (boolean must be true iff it is a record) *) -val declare_mind : internal_flag -> mutual_inductive_entry -> object_name + the whole block and a boolean indicating if it is a primitive record. *) +val declare_mind : mutual_inductive_entry -> object_name * bool (** Declaration messages *) |