diff options
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -197,8 +197,6 @@ Extensions de syntaxe avec Grammar et Syntax - Le non affichage des Infix est corrigé. - Ajout d'une syntaxe pour les réels: ``Rexpr``. - Point noir dû aux constantes: (Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1) - est toujours (2+2+1) au lieu de 2+2+1 Syntaxe des constructions @@ -315,6 +313,12 @@ Tactiques La tactique a été instantiée pour les nombres réels et peut donc être utilisée pour résoudre des égalités sur les réels. +- Nouveau: tactique Fourier qui résoud les inégalités linéaires sur les + nombres réels. + +- Nouveau: diverses tactiques pour les nombres réels: DiscrR, SplitRmult, + SplitAbsolu. + Outils - Deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; |