Commit 7c7797db authored by MARCHE Claude's avatar MARCHE Claude

adjust for supporting both Coq 8.5 and Coq 8.6

parent e07b4d55
......@@ -32,10 +32,13 @@ Require Import ZArith.
Require Import Fourier.
Require Import real.Truncate.
Arguments B754_zero {prec} {emax}.
Arguments B754_infinity {prec} {emax}.
Arguments B754_nan {prec} {emax}.
Arguments B754_finite {prec} {emax}.
(* extra arguments _ below are needed for Coq prior to 8.6
keep them until support for Coq 8.5 is dropped *)
Arguments B754_zero {prec} {emax} _ .
Arguments B754_infinity {prec} {emax} _.
Arguments B754_nan {prec} {emax} _ _ .
Arguments B754_finite {prec} {emax} _ _ _ _ .
(* Why3 assumption *)
Inductive mode :=
......
......@@ -600,7 +600,7 @@ command = "%l/why3-call-pvs %l pvs %f"
[editor coqide]
name = "CoqIDE"
command = "coqide -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
command = "coqide -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
[editor proofgeneral-coq]
name = "Emacs/ProofGeneral/Coq"
......
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