summaryrefslogtreecommitdiff
path: root/toplevel/classes.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /toplevel/classes.mli
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'toplevel/classes.mli')
-rw-r--r--toplevel/classes.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 0a351d3c..2b7e9e4f 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -8,7 +8,6 @@
open Names
open Context
-open Evd
open Environ
open Constrexpr
open Typeclasses
@@ -33,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