diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:11:04 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:11:04 +0100 |
| commit | ff947d85f8b8921e401b693e47c52504c71f9c4c (patch) | |
| tree | 24c7acce3d8dcc2d5babb7182f81924bb4ae82cd /vernac | |
| parent | 0c345d64d67c01c7b7a75bf23391b421f95c4fb7 (diff) | |
| parent | 925487d5450f2575b1d46a9a694c5e447c776047 (diff) | |
Merge PR #6945: Fix error with univ binders on monomorphic records.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index e21f53f55..6e745b2af 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -594,13 +594,12 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in - let gr = match kind with + match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities in - gr - | _ -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + declare_class finite def cum pl univs (loc,idstruc) idbuild + implpars params arity template implfs fields is_coe coers priorities + | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs @@ -618,7 +617,4 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind - in - Declare.declare_univ_binders gr pl; - gr + IndRef ind |