diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 9d4e9d68d..fc2c2cb29 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -361,10 +361,10 @@ let interp_mutual lparams lnamearconstrs finite = notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec } with e -> States.unfreeze fs; raise e -let declare_mutual_with_eliminations mie = +let declare_mutual_with_eliminations isrecord mie = let lrecnames = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_,kn) = declare_mind mie in + let (_,kn) = declare_mind isrecord mie in if_verbose ppnl (minductive_message lrecnames); declare_eliminations kn; kn @@ -406,7 +406,7 @@ let extract_coe_la_lc = function let build_mutual lind finite = let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in let notations,mie = interp_mutual lparams lnamearconstructs finite in - let kn = declare_mutual_with_eliminations mie in + let kn = declare_mutual_with_eliminations false mie in (* Declare the notations now bound to the inductive types *) List.iter (fun (df,c,scope) -> Metasyntax.add_notation_interpretation df [] c scope) notations; diff --git a/toplevel/command.mli b/toplevel/command.mli index c2db70daf..77eff2b4d 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -41,7 +41,7 @@ val declare_assumption : identifier located list -> val build_mutual : inductive_expr list -> bool -> unit val declare_mutual_with_eliminations : - Entries.mutual_inductive_entry -> mutual_inductive + bool -> Entries.mutual_inductive_entry -> mutual_inductive val build_recursive : (fixpoint_expr * decl_notation) list -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 36d83bb28..acddd2e61 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -228,7 +228,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let mie = { mind_entry_finite = true; mind_entry_inds = [mie_ind] } in - let sp = declare_mutual_with_eliminations mie in + let sp = declare_mutual_with_eliminations true mie in let rsp = (sp,0) in (* This is ind path of idstruc *) let sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) |