From: Andrea Asperti Date: Fri, 9 Apr 2010 14:04:08 +0000 (+0000) Subject: apply_subst_context on statuses X-Git-Tag: make_still_working~2933 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c4228417fc38e71bce647174d175561db2afb01;p=helm.git apply_subst_context on statuses From: asperti --- 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