From: Claudio Sacerdoti Coen Date: Mon, 6 Apr 2009 19:59:21 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4112 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=477d9f8e1cb71dd2915ec92fa0bf963ef96d1bdc;p=helm.git ... --- 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).