From 18d8d7128c16b5d4dd589d75a2e7c026ac7d405d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 10:20:39 +0000 Subject: [PATCH] added mk_fix i j r that given an r of a fix generated another fix on i and j --- 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 2692075e0..5da330541 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -119,6 +119,12 @@ let mk_constructor j = function | _ -> assert false ;; +let mk_fix i j = function + | Ref (d, u, Fix _) -> + reference_of_string (string_of_reference (Ref (d, u, Fix (i,j)))) + | _ -> 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 de468c3c1..752853608 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -28,6 +28,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 (* CACCA *) -- 2.39.2