Les records déclarés avec Record ne peuvent plus être récursifs (le

comportement est similaire à la 8.1). Les records récursifs peuvent-être 
déclarés avec Inductive et CoInductive, avec les effets idoines sur leur 
nature.

J'ai fait quelques changements dans VernacInductive pour que tout ceci 
fonctionne bien ensemble. Il reste du nettoyage à faire et probablement 
des ajustement dans le Printing.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11808 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 735a8fb07..03b14e31c 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -112,3 +112,18 @@ let strength_of_global = function
 let string_of_strength = function
   | Local -> "Local"
   | Global -> "Global"
+
+
+(* Recursive power *)
+
+(* spiwack: this definition might be of use in the kernel, for now I do not
+                   push them deeper than needed, though. *)
+type recursivity_kind =
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+let recursivity_flag_of_kind = function
+  | Finite | BiFinite -> true
+  | CoFinite -> false