Commit aa53b02a authored by MARCHE Claude's avatar MARCHE Claude

a few adjustments after Why3 GT

parent 53f53265
......@@ -76,6 +76,7 @@ let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
monomorphic, since it is checked by typing *)
List.fold_left (fun acc (ls,_) -> acc || check_ls ign_ls ls) false indl
| Dprop (_,pr,t) ->
(* todo: NE PAS TESTER le goal *)
not (Spr.mem pr ign_pr) &&
let s = Term.t_ty_freevars Ty.Stv.empty t in
not (Ty.Stv.is_empty s)
......
......@@ -1281,7 +1281,10 @@ and exec_app env s ps args (*spec*) ity_result =
Mreg.filter (fun r1 r2 -> not (reg_equal r1 r2)) subst
in
let env1 = { env with regenv =
(*
Mreg.union (fun _ x _ -> Some x) subst env.regenv }
*)
Mreg.set_union subst env.regenv
in
match find_definition env ps with
| Some d ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment