aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 805a29e39..e750f0ca2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
Evarutil.check_evars env Evd.empty !evars termtype;
let 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