diff options
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 20690fa8..ba40f98c 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Libnames @@ -17,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -54,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -86,12 +82,12 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (l,boxed,d) = - match (l,d) with +let string_of_definition_kind def = + match def with | Local, Coercion -> "Coercion Local" | Global, Coercion -> "Coercion" | Local, Definition -> "Let" - | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Global, Definition -> "Definition" | Local, SubClass -> "Local SubClass" | Global, SubClass -> "SubClass" | Global, CanonicalStructure -> "Canonical Structure" |