diff options
Diffstat (limited to 'contrib/correctness/pcicenv.ml')
| -rw-r--r-- | contrib/correctness/pcicenv.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml index c1b4b0fa3..4663b3e37 100644 --- a/contrib/correctness/pcicenv.ml +++ b/contrib/correctness/pcicenv.ml @@ -24,14 +24,17 @@ open Past (* VERY UGLY!! find some work around *) let modify_sign id t s = - let t' = lookup_id_type id s in - map_named_context (fun t'' -> if t'' == t' then t else t'') s + fold_named_context + (fun ((x,b,ty) as d) sign -> + if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign) + s empty_named_context let add_sign (id,t) s = - if mem_named_context id s then + try + let _ = lookup_named id s in modify_sign id t s - else - add_named_assum (id,t) s + with Not_found -> + add_named_decl (id,None,t) s let cast_set c = mkCast (c, mkSet) |