diff options
| author | Vincent Laporte | 2018-11-16 11:40:49 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-11-27 09:14:43 +0000 |
| commit | b2ed1bffb7601f6bcaf3a73c110a2783451a6e26 (patch) | |
| tree | 65d86f34e6ba21becd03a2e9ba0b76b9fb7f747d | |
| parent | 5fcf1b7dcd9b20ea7c5ad317ce2bfe4fbb5452d9 (diff) | |
Record.declare_class: remove unused “finite” parameter
| -rw-r--r-- | vernac/record.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 7bdf6a973f..669e7a33a4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -458,7 +458,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum ubinders univs id idbuild paramimpls params arity +let declare_class def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records = in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum ubinders univs id.CAst.v idbuild + declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in |