From 1dde0b0d0738439b29d7c2e4be9b9cbc382e8d5e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 16:28:50 +0000 Subject: [PATCH] Bug fixed: the `IsTerm attribute is now added by mk_meta and it was not preserved. The current code should be more stable. --- helm/software/components/ng_tactics/nTacStatus.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 0bef3a794..b6013c272 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -267,6 +267,7 @@ let mk_meta status ?(attrs=[]) ctx bo_or_ty kind = let n,h,metasenv,subst,o = status#obj in let metasenv, metano, instance, _ = NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in + let attrs,_,_ = NCicUtils.lookup_meta metano metasenv in let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in let status = status#set_obj (n,h,metasenv,subst,o) in -- 2.39.2