From 16fc013c83981bb5c2bb24ac4e06bc0ca1fda80d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 17 May 2009 19:13:03 +0000 Subject: [PATCH] maxmeta function to return the heighest meta used so far --- helm/software/components/ng_refiner/nCicMetaSubst.mli | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 3378aa998..7bde2c1d6 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -14,6 +14,9 @@ exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t +(* the index of the last created meta *) +val maxmeta: unit -> int + (* the delift function takes in input a metavariable index, a local_context * and a term t, and substitutes every subterm t' of t with its position * (searched up-to unification) in -- 2.39.2