From dc83d986afedb519551b2509faa9f58e5baf022c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 25 Apr 2009 20:29:06 +0000 Subject: [PATCH] Apply subst implemented also for Fixpoints. --- helm/software/components/ng_tactics/nTacStatus.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index f0b00e561..eeca351c2 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -352,6 +352,14 @@ let apply_subst_obj subst = NCic.Constant (relev,name,HExtlib.map_option (apply_subst subst []) bo, apply_subst subst [] ty,attrs) + | NCic.Fixpoint (ind,fl,attrs) -> + let fl = + List.map + (function (relevance,name,recno,ty,bo) -> + relevance,name,recno,apply_subst subst [] ty,apply_subst subst [] bo + ) fl + in + NCic.Fixpoint (ind,fl,attrs) | _ -> assert false (* not implemented yet *) ;; -- 2.39.2