Outils pour utilisateurs

Outils du site


lang:coq:mise_a_jour

Différences

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

Lien vers cette vue comparative

Les deux révisions précédentesRévision précédente
Prochaine révision
Révision précédente
lang:coq:mise_a_jour [2020/03/14 22:28] – Ajout de "Implicit Arguments" rootlang: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''. 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   Ncompare
  
-Après :+A partir de la version Coq 8.10 :
  
   N.compare   N.compare
Ligne 16: Ligne 16:
  
   The constructor XXX (in type yyy) expects 1 argument.   The constructor XXX (in type yyy) expects 1 argument.
- 
  
 Avant : Avant :
Ligne 42: Ligne 41:
   Syntax error: 'Type' or 'Types' expected after 'Implicit' (in [vernac:gallina_ext]).   Syntax error: 'Type' or 'Types' expected after 'Implicit' (in [vernac:gallina_ext]).
  
-Avant :+Jusqu'à la version Coq 8.8 :
  
 <code> <code>
Ligne 48: Ligne 47:
 </code> </code>
  
-Après :+A partir de la version Coq 8.9 :
  
 <code> <code>
 Arguments every_other_even [A]. 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> </code>
lang/coq/mise_a_jour.1584221300.txt.gz · Dernière modification : 2020/03/14 22:28 de root