diff options
| author | Pierre-Marie Pédrot | 2015-10-29 13:04:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 13:11:38 +0100 |
| commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
| tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /toplevel/classes.ml | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 439e20a86b..0a10cfdc36 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -186,9 +186,9 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro nf t in Evarutil.check_evars env Evd.empty !evars termtype; - let ctx = Evd.universe_context !evars in + let pl, ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (Entries.ParameterEntry + (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id end @@ -382,7 +382,7 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, !uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) in let () = uctx := Univ.ContextSet.empty in |