From 72f2faebd85bf6a191325b1ac39f051b22e8d838 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jun 2005 16:53:21 +0000 Subject: [PATCH] added mk_rel --- helm/ocaml/cic/cicUtil.ml | 5 +++++ helm/ocaml/cic/cicUtil.mli | 4 ++++ 2 files changed, 9 insertions(+) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 5a64429a3..e686b6b35 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -278,4 +278,9 @@ let attributes_of_obj = function | Cic.CurrentProof (_, _, _, _, _, attributes) | Cic.InductiveDefinition (_, _, _, attributes) -> attributes + +let rec mk_rels howmany from = + match howmany with + | 0 -> [] + | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 650758eed..0bf193e7d 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -68,3 +68,7 @@ val context_of: * rooted at context's holes *) val select: term:Cic.term -> context:Cic.term -> Cic.term list +(** mk_rels [howmany] [from] + * creates a list of [howmany] rels starting from [from] in decreasing order *) +val mk_rels : int -> int -> Cic.term list + -- 2.39.2