Commit 32cdfb78 authored by MARCHE Claude's avatar MARCHE Claude

"tan" and "atan" in Coq 8.4

parent d926138c
...@@ -276,30 +276,5 @@ theory real.PowerInt ...@@ -276,30 +276,5 @@ theory real.PowerInt
end end
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)"
syntax function cos "(Rtrigo_def.cos %1)"
syntax function sin "(Rtrigo_def.sin %1)"
syntax function pi "PI"
syntax function tan "(Rtrigo.tan %1)"
(* syntax function atan "atan not defined in Coq ?" *)
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
(* this file has an extension .aux rather than .gen since it should not be distributed *) (* this file has an extension .aux rather than .gen since it should not be distributed *)
import "coq-realizations.aux" import "coq-realizations.aux"
...@@ -6,3 +6,29 @@ printer "coq" ...@@ -6,3 +6,29 @@ printer "coq"
filename "%f_%t_%g.v" filename "%f_%t_%g.v"
import "coq-common.gen" import "coq-common.gen"
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)"
syntax function cos "(Rtrigo_def.cos %1)"
syntax function sin "(Rtrigo_def.sin %1)"
syntax function pi "PI"
syntax function tan "(Rtrigo.tan %1)"
(* syntax function atan "atan not defined in Coq ?" *)
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
prelude "(* This file is generated by Why3's Coq 8.4 driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq"
filename "%f_%t_%g.v"
import "coq-common.gen"
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)"
syntax function cos "(Rtrigo_def.cos %1)"
syntax function sin "(Rtrigo_def.sin %1)"
syntax function pi "PI"
syntax function tan "(Rtrigo1.tan %1)"
syntax function atan "(Ratan.atan %1)"
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
...@@ -319,6 +319,15 @@ exec = "coqtop -batch" ...@@ -319,6 +319,15 @@ exec = "coqtop -batch"
version_switch = "-v" version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.4" version_ok = "8.4"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq_8_4.drv"
editor = "coqide"
[ITP coq]
name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.3pl4" version_ok = "8.3pl4"
version_ok = "8.3pl3" version_ok = "8.3pl3"
version_ok = "8.3pl2" version_ok = "8.3pl2"
......
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