Différences

Ci-dessous, les différences entre deux révisions de la page.

--- lang:coq:mise_a_jour [2020/03/14 21:54] – Ajout de "_ doit être mis après with" root
+++ lang:coq:mise_a_jour [2020/03/19 21:09] (Version actuelle) – Ajout de "SearchAbout" qui devient "Search" root
@@ Ligne 3: / Ligne 3: @@
 Voir commit ''b1162463d577baf450c3f33ab880e7d9afe21148''. Les fonctions commençant par ''N'', ''P'' ou 'Z'' ont été déplacées dans leur propre ''namespace''.
-Avant :
+Jusqu'à la version Coq 8.9 :
   Ncompare
-Après :
+A partir de la version Coq 8.10 :
   N.compare
@@ Ligne 13: / Ligne 13: @@
 ===_ doit être mis après match ... with===
-Message :
+Message d'erreur :
   The constructor XXX (in type yyy) expects 1 argument.
 Avant :
@@ Ligne 34: / Ligne 33: @@
   | N' _ x t t' => t'
   end.
+</code>
+===Implicit Arguments===
+Message d'erreur :
+  Syntax error: 'Type' or 'Types' expected after 'Implicit' (in [vernac:gallina_ext]).
+Jusqu'à la version Coq 8.8 :
+<code>
+Implicit Arguments every_other_even [A].
+</code>
+A partir de la version Coq 8.9 :
+<code>
+Arguments every_other_even [A].
+</code>
+===SearchAbout===
+Jusqu'à la version Coq 8.11 :
+<code>
+SearchAbout leb.
+</code>
+Après la version Coq 8.11 :
+<code>
+Search leb.
 </code>