From b0dee52bfa97405adc7c0dbffa0f3558f349659e Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Wed, 30 May 2018 11:33:37 +0200
Subject: Define rec_declaration in terms of prec_declaration. And similarly
 for fixpoint and cofixpoint.

---
 kernel/constr.ml  | 16 ++++------------
 kernel/constr.mli | 30 +++++++++++++++++++++---------
 2 files changed, 25 insertions(+), 21 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index c11b9ebf4..418229330 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term
 type constr = t
 
 type existential = existential_key * constr array
-type rec_declaration = Name.t array * constr array * constr array
-type fixpoint = (int array * int) * rec_declaration
-  (* The array of [int]'s tells for each component of the array of
-     mutual fixpoints the number of lambdas to skip before finding the
-     recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
-     (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
-     the recursive argument);
-     The second component [int] tells which component of the block is
-     returned *)
-type cofixpoint = int * rec_declaration
-  (* The component [int] tells which component of the block of
-     cofixpoint is returned *)
 
 type types = constr
 
+type rec_declaration = (constr, types) prec_declaration
+type fixpoint = (constr, types) pfixpoint
+type cofixpoint = (constr, types) pcofixpoint
+
 (*********************)
 (* Term constructors *)
 (*********************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 742a13919..bf7b5e87b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr
 
    where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
 *)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
+type ('constr, 'types) prec_declaration =
+    Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+    (int array * int) * ('constr, 'types) prec_declaration
+  (* The array of [int]'s tells for each component of the array of
+     mutual fixpoints the number of lambdas to skip before finding the
+     recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+     (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+     the recursive argument);
+     The second component [int] tells which component of the block is
+     returned *)
+
+type ('constr, 'types) pcofixpoint =
+    int * ('constr, 'types) prec_declaration
+  (* The component [int] tells which component of the block of
+     cofixpoint is returned *)
+
+type rec_declaration = (constr, types) prec_declaration
+
+type fixpoint = (constr, types) pfixpoint
 val mkFix : fixpoint -> constr
 
 (** If [funnames = [|f1,.....fn|]]
@@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr
      ...
      with       fn = bn.]
  *)
-type cofixpoint = int * rec_declaration
+type cofixpoint = (constr, types) pcofixpoint
 val mkCoFix : cofixpoint -> constr
 
 
@@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr
 (** [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr pexistential = Evar.t * 'constr array
-type ('constr, 'types) prec_declaration =
-    Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
-    (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
-    int * ('constr, 'types) prec_declaration
 
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int                                  (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
-- 
cgit v1.2.3