From 33496369f0ee2a45c390aa69623fc0474324c6e3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Oct 2009 15:54:13 +0000 Subject: [PATCH] New function. --- helm/software/components/ng_kernel/nCicUntrusted.ml | 6 ++++++ helm/software/components/ng_kernel/nCicUntrusted.mli | 3 +++ 2 files changed, 9 insertions(+) diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 771f3070b..8c827a759 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -264,6 +264,12 @@ let rec replace_in_metasenv i f = function | x::tl -> x :: replace_in_metasenv i f tl ;; +let rec replace_in_subst i f = function + | [] -> assert false + | (j,e)::tl when j=i -> (i,f e) :: tl + | x::tl -> x :: replace_in_subst i f tl +;; + let set_kind newkind attrs = newkind :: List.filter (fun x -> not (is_kind x)) attrs ;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 9f5ab0fd5..aa71e05d4 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -25,6 +25,9 @@ val kind_of_meta: NCic.meta_attrs -> meta_kind val set_kind: meta_kind -> NCic.meta_attrs -> NCic.meta_attrs val replace_in_metasenv: int -> (NCic.conjecture -> NCic.conjecture) -> NCic.metasenv -> NCic.metasenv +val replace_in_subst: + int -> (NCic.subst_entry -> NCic.subst_entry) -> NCic.substitution -> + NCic.substitution val max_kind: meta_kind -> meta_kind -> meta_kind module NCicHash : Hashtbl.S with type key = NCic.term -- 2.39.2