diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-08 14:04:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-08 16:24:49 +0100 |
| commit | 925487d5450f2575b1d46a9a694c5e447c776047 (patch) | |
| tree | d3b77829a0dc31d89b208a2430c0b31362b00412 /vernac/record.ml | |
| parent | 563199757c5756fb5858da1b684162566a73fa3e (diff) | |
Fix error with univ binders on monomorphic records.
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
Diffstat (limited to 'vernac/record.ml')
| -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 |