localize logical expressions in programs

src/programs/pgm_env.ml

@@ -174,10 +174,8 @@ let parse_string f loc s =
   reloc loc lb;
   f lb
 
-let logic_lexpr ((pos, _) as loc, s) = 
-  let e = parse_string Lexer.parse_lexpr pos s in
-  let lab = Ident.label ~loc "annotation" in
-  { e with Ptree.pp_desc = Ptree.PPnamed (lab, e) }
+let logic_lexpr ((pos, _), s) =
+  parse_string Lexer.parse_lexpr pos s
 
 let logic_decls ((loc, _), s) e env =
   let parse = Lexer.parse_list0_decl e Mnm.empty env.uc in

src/programs/pgm_typing.ml

@@ -203,8 +203,8 @@ let deffect env e =
       List.map (fun id -> let ls,_,_ = dexception env id in ls) 
 	e.Pgm_ptree.pe_raises; }
 
-let dterm env l = Typing.dterm env (Pgm_env.logic_lexpr l)
-let dfmla env l = Typing.dfmla env (Pgm_env.logic_lexpr l)
+let dterm env l = Typing.dterm ~localize:true env (Pgm_env.logic_lexpr l)
+let dfmla env l = Typing.dfmla ~localize:true env (Pgm_env.logic_lexpr l)
 
 let dpost env ty (q, ql) =
   let dexn (id, l) =