diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 214d44d83f..c9b46983e7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -361,7 +361,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure chk finite poly ctx id idbuild paramimpls params arity template +let declare_structure finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list nfields params in @@ -387,7 +387,8 @@ let declare_structure chk finite poly ctx id idbuild paramimpls params arity tem mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx; - mind_entry_check_positivity = chk; } in + } + in let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in @@ -406,7 +407,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map get_name ctx))) -let declare_class chk finite def poly ctx id idbuild paramimpls params arity +let declare_class finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -449,7 +450,7 @@ let declare_class chk finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -528,9 +529,8 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions - or subinstances. When [chk] is false positivity is - assumed. *) -let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = + or subinstances. *) +let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in @@ -551,14 +551,14 @@ let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf let sign = structure_signature (fields@params) in let gr = match kind with | Class def -> - let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure chk finite poly ctx idstruc + let ind = declare_structure finite poly ctx idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind |