From 54b8cadfb5884357cc3f9df1359512624f5a9191 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 May 2008 16:42:12 +0000 Subject: [PATCH] added mk_cofix --- helm/software/components/ng_kernel/nReference.ml | 6 ++++++ helm/software/components/ng_kernel/nReference.mli | 1 + 2 files changed, 7 insertions(+) diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 5da330541..edb69c7bf 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -125,6 +125,12 @@ let mk_fix i j = function | _ -> assert false ;; +let mk_cofix i = function + | Ref (d, u, CoFix _) -> + reference_of_string (string_of_reference (Ref (d, u, CoFix i))) + | _ -> assert false +;; + let reference_of_ouri u indinfo = let u = NUri.nuri_of_ouri u in reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index 752853608..1ed27e94d 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -29,6 +29,7 @@ val string_of_reference: reference -> string (* given the reference of an inductive type, returns the i-th contructor *) val mk_constructor: int -> reference -> reference val mk_fix: int -> int -> reference -> reference +val mk_cofix: int -> reference -> reference (* CACCA *) -- 2.39.2