diff options
| author | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
| commit | 148cf78a4d85ec56818a8ff00719a775670950b9 (patch) | |
| tree | ea4540bb896b3bbedb7c41b80fcf7e0ff1cd04aa /toplevel | |
| parent | 429f493997e34bfaac930c68bf6b267a5b9640ee (diff) | |
| parent | 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 9 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 |
3 files changed, 9 insertions, 4 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 07f881721d..33891ad94c 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id poly uctx term termtype = let kind = IsDefinition Instance in + let uctx = + let levels = Univ.LSet.union (Universes.universes_of_constr termtype) + (Universes.universes_of_constr term) in + Universes.restrict_universe_context uctx levels + in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then - let ctx = Evd.universe_context evm in + let ctx = Evd.universe_context_set evm in declare_instance_constant k pri global imps ?hook id poly ctx (Option.get term) termtype else if !refine_instance || Option.is_empty term then begin diff --git a/toplevel/classes.mli b/toplevel/classes.mli index cb88ae564d..2b7e9e4fe2 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -32,7 +32,7 @@ val declare_instance_constant : ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) bool -> (* polymorphic *) - Univ.universe_context -> (* Universes *) + Univ.universe_context_set -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) Names.Id.t diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 456a6f9d0f..523134b50f 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -658,7 +658,7 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls Array.mapi (fun i (n, t, l, o, d, tac) -> { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; + obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in |