From 477d9f8e1cb71dd2915ec92fa0bf963ef96d1bdc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 6 Apr 2009 19:59:21 +0000 Subject: [PATCH] ... --- .../components/ng_refiner/nCicMetaSubst.mli | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 1ed2fcee3..f7378d13b 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -14,20 +14,6 @@ exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t -(* -exception AssertFailure of string Lazy.t -exception DeliftingARelWouldCaptureAFreeVariable;; -val apply_subst : Cic.substitution -> Cic.term -> Cic.term -val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context -val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv - -(*** delifting ***) - -val restrict : - Cic.substitution -> (int * int) list -> Cic.metasenv -> - Cic.metasenv * Cic.substitution -*) - (* the delift function takes in input a metavariable index, a local_context * and a term t, and substitutes every Rel in t with its position in * the local_context (which is the Rel moved to the canonical context). -- 2.39.2