diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 15:46:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (patch) | |
| tree | 628fd2161dcc0fcfabe9499669ee932d7878b63d /vernac | |
| parent | 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (diff) | |
Use Maps and ids for universe binders
Before sometimes there were lists and strings.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 4 | ||||
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 20cb43b24..ed37bab6d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -411,14 +411,14 @@ let context poly l = let decl = (Discharge, poly, Definitional) in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let ctx = Univ.ContextSet.to_context !uctx in let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = DeclareDef.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/command.ml b/vernac/command.ml index 257c003b5..5d83de070 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 nf_evar) l in pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) Universes.empty_binders imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a44de66e9..590332d08 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -484,7 +484,7 @@ let declare_definition prg = let () = progmap_remove prg in let cst = DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce [] prg.prg_implicits + prg.prg_kind ce Universes.empty_binders prg.prg_implicits (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) in Universes.register_universe_binders cst pl; @@ -554,7 +554,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; 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 = |