Commit f18df802 authored by MARCHE Claude's avatar MARCHE Claude

a few fix after meeting with D Mentré

parent 911263f3
......@@ -77,6 +77,7 @@ NON PRIORITAIRE ?
** Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
** fix CVC3 printer: prints predicate def using LAMBDA
* FRANCOIS CLAUDE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
......
......@@ -11,7 +11,7 @@ Definition set : forall (a:Type), Type.
(* YOU MAY EDIT THE PROOF BELOW *)
exact set_.
(*
(fun (X: Type) => X -> Prop).
exact (fun (X: Type) => X -> Prop).
*)
Defined.
(* DO NOT EDIT BELOW *)
......
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