Commit b87527c5 authored by MARCHE Claude's avatar MARCHE Claude

fix Coq version

parent 14829503
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Inductive t :=
| T : t .
Inductive x (a:Type) (b:Type) :=
| X : t -> a -> x a b
| Y : t -> b -> x a b.
Set Contextual Implicit.
Implicit Arguments X.
Unset Contextual Implicit.
Set Contextual Implicit.
Implicit Arguments Y.
Unset Contextual Implicit.
Inductive a :=
| A0 : a
| A1 : a .
Inductive b :=
| B : b .
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem x1 : ((X T A0:(x a b)) = (X T A1:(x a b))).
(* YOU MAY EDIT THE PROOF BELOW *)
admit.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13849/why3session.xml">
name="examples/bts/13849/why3session.xml">
<prover
id="0"
name="Coq"
version="8.2pl2"/>
version="8.3pl3"/>
<file
name="../13849.why"
verified="false"
verified="true"
expanded="true">
<theory
name="T"
locfile="13849/../13849.why"
locfile="examples/bts/13849/../13849.why"
loclnum="4" loccnumb="7" loccnume="8"
verified="false"
verified="true"
expanded="true">
<goal
name="x"
locfile="13849/../13849.why"
locfile="examples/bts/13849/../13849.why"
loclnum="19" loccnumb="6" loccnume="7"
sum="15dd0a14b365705789dc555517dcc6cd"
proved="false"
proved="true"
expanded="true"
shape="ainfix =ab1ab2">
<proof
prover="0"
timelimit="10"
edited="13849_T_x_1.v"
obsolete="true"
archived="false"><unedited/>
edited="13849_T_x_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.46"/>
</proof>
</goal>
</theory>
......
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