aboutsummaryrefslogtreecommitdiff
path: root/toplevel/classes.mli
diff options
context:
space:
mode:
authormsozeau2011-04-13 14:29:02 +0000
committermsozeau2011-04-13 14:29:02 +0000
commit60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (patch)
tree0eeffe9b7b098ad653ffeb6ad963c62223245d0e /toplevel/classes.mli
parent3b11686e4f78f6d166f84d990ac4fedb4d3e800a (diff)
Revert "Add [Polymorphic] flag for defs"
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/classes.mli')
-rw-r--r--toplevel/classes.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 5ef5feffd5..b57f1bea07 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
bool -> (** globality *)
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Libnames.global_reference -> unit) ->
- polymorphic ->
identifier -> (** name *)
Term.constr -> (** body *)
Term.types -> (** type *)
@@ -49,7 +48,6 @@ val declare_instance_constant :
val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
- polymorphic ->
local_binder list ->
typeclass_constraint ->
constr_expr option ->