aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-15 15:46:30 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-24 19:18:56 +0100
commitd437078a4ca82f7ca6d19be5ee9452359724f9a0 (patch)
tree628fd2161dcc0fcfabe9499669ee932d7878b63d /vernac/record.ml
parent485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (diff)
Use Maps and ids for universe binders
Before sometimes there were lists and strings.
Diffstat (limited to 'vernac/record.ml')
-rw-r--r--vernac/record.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml
index f09b57048..6ffbd1584 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -426,7 +426,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template
else
mie
in
- let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
+ let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
let fields =