Commit 796fb59a authored by MARCHE Claude's avatar MARCHE Claude

fix bts 13854

parent 5839c12a
* marks an incompatible change * marks an incompatible change
o fix BTS 13854
o fix BTS 13849
o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
introduce constants, as an alternative to "function" introduce constants, as an alternative to "function"
......
theory T
type t 'a = A 'a | B
function f () : ()
goal g : () = f ()
goal x : A () <> B
(*Theorem x : ((A ) = (B :(t unit))). *)
end
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive t (a:Type) :=
| A : a -> t a
| B : t a.
Implicit Arguments A.
Set Contextual Implicit.
Implicit Arguments B.
Unset Contextual Implicit.
Parameter f: unit -> unit.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem g : (tt = (f tt)).
(* YOU MAY EDIT THE PROOF BELOW *)
destruct (f tt); auto.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive t (a:Type) :=
| A : a -> t a
| B : t a.
Implicit Arguments A.
Set Contextual Implicit.
Implicit Arguments B.
Unset Contextual Implicit.
Parameter f: unit -> unit.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem x : ~ ((A tt) = (B :(t unit))).
(* YOU MAY EDIT THE PROOF BELOW *)
discriminate.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13854/why3session.xml">
<prover
id="0"
name="Coq"
version="8.3pl3"/>
<file
name="../13854.why"
verified="true"
expanded="true">
<theory
name="T"
locfile="13854/../13854.why"
loclnum="1" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="g"
locfile="13854/../13854.why"
loclnum="6" loccnumb="7" loccnume="8"
sum="54a27536c38d94e56a04e1a84c5f21e6"
proved="true"
expanded="true"
shape="ainfix =aTuple0afaTuple0">
<proof
prover="0"
timelimit="5"
edited="13854_T_g_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
name="x"
locfile="13854/../13854.why"
loclnum="8" loccnumb="7" loccnume="8"
sum="0c0178555cd601b6589cfe58c26d04bb"
proved="true"
expanded="true"
shape="ainfix =aAaTuple0aBN">
<proof
prover="0"
timelimit="5"
edited="13854_T_x_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
</goal>
</theory>
</file>
</why3session>
...@@ -260,6 +260,8 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -260,6 +260,8 @@ and print_tnode opl opr info fmt t = match t.t_node with
fprintf fmt (protect_on opr "epsilon %a.@ %a") fprintf fmt (protect_on opr "epsilon %a.@ %a")
(print_vsty info) v (print_opl_fmla info) f; (print_vsty info) v (print_opl_fmla info) f;
forget_var v forget_var v
| Tapp (fs,[]) when is_fs_tuple fs ->
fprintf fmt "tt"
| Tapp (fs,pl) when is_fs_tuple fs -> | Tapp (fs,pl) when is_fs_tuple fs ->
fprintf fmt "%a" (print_paren_r (print_term info)) pl fprintf fmt "%a" (print_paren_r (print_term info)) pl
| Tapp (fs, tl) -> | Tapp (fs, tl) ->
......
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