From 4c4228417fc38e71bce647174d175561db2afb01 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 9 Apr 2010 14:04:08 +0000 Subject: [PATCH] apply_subst_context on statuses From: asperti --- helm/software/components/ng_tactics/nTacStatus.ml | 5 +++++ helm/software/components/ng_tactics/nTacStatus.mli | 2 ++ 2 files changed, 7 insertions(+) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 280634d30..1aaeb50f6 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -424,6 +424,11 @@ let apply_subst status ctx t = status, (ctx, NCicUntrusted.apply_subst subst ctx t) ;; +let apply_subst_context status ~fix_projections ctx = + let _,_,_,subst,_ = status#obj in + NCicUntrusted.apply_subst_context ~fix_projections subst ctx +;; + let metas_of_term status (context,t) = let _,_,_,subst,_ = status#obj in NCicUntrusted.metas_of_term subst context t diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index ad9df5256..561679457 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -63,6 +63,8 @@ val refine: 'status * cic_term * cic_term (* status, term, type *) val apply_subst: #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term +val apply_subst_context : + #pstatus -> fix_projections:bool -> NCic.context -> NCic.context val fix_sorts: #pstatus as 'status -> cic_term -> 'status * cic_term val saturate : #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list -- 2.39.2