Métathéorie

- Ajout de définitions locales (Let-In)

Parsing

- Le Lexeur considère maintenant comme token toute suite de symboles
(source d'incompatibilité : il faut insérer des espaces entre tokens
spéciaux consécutifs)

- "command" in grammars and quotations is now "constr" as in
  pretty-printing rules

Syntaxe des constructions

- Consecutive as in patterns are forbidden

- Names generated in Cases are different (source d'incompatibilité)
  Consecutive 'as' in patterns are forbidden

- Davantage d'inférence automatique de "?".

- Davantage d'arguments implicites engendrés par le discharge.

- Les cas des Cases ne se lisent plus de manière séquentielle, sauf en
  cas de clauses par défaut redondantes auquel cas la première est prise
  avec un avertissement.

Syntaxe des theories

- Ajout d'une syntaxe pour les reels: ``Rexpr``.
  Point noir du aux constantes: 
     (Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1) est toujours (2+2+1) 
               au lieu de 2+2+1 

Vernac

- Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
phrases (utile pour Time et pour des grammaires abrégeant plusieurs
commandes)

- Le parseur par défaut des actions des règles de grammaires et des
motifs des règles d'affichage est maintenant celui associé au nom de
la grammaire (vernac, tactic ou constr). Donc plus de piquants
<:vernac:<...>> etc. Pour retourner de l'ast, il faut typer
explicitement la grammaire avec "ast" ou "List" (renommé d'ailleurs
"ast list"), ou, si c'est dans une règle Syntax, utiliser la quotation
<< ... >> qui replace dans ast. Pour les nouvelles grammaires (autre
que les 3 primitives), on peut typer avec "constr", "tactic", ou
"vernac" pour utiliser le parseur correspondant.

- AddPath -> Add Path;
  Print LoadPath -> Print Path;
  DelPath -> Remove Path;
  Print Path -> Print Coercion Paths.

- Bug affichage Infix corrigé

- Légère restriction de la syntaxe de Cbv Delta

- L'option [-myconst] de Cbv doit immédiatement suivre Delta

- End Silent etait interprete comme une fin de section 
  Begin Silent -> Set Silent
  End Silent -> Unset Silent.

- Déclaration manuelle des implicites avec

	Implicits ident.
	Implicits ident [ num num ... num ].

  Petit changement de sémantique : lors de la fermeture d'une section,
  les implicites sont calculés selon la valeur *courante* de "Implicit 
  Arguments" et non plus selon la valeur qu'elle avait au moment de la 
  définition dans la section.

- SearchPattern / SearchRewrite (contrib de Yves Bertot)

Tactiques

- Langage de tactique

- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"

- Decompose :
  - Numérotation dans l'ordre des hypothèses créées
  - Correction de bugs (quand le type ne commence pas par un inductif)
    et refus d'agir sous les ->.

- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. En
  revanche, si une constante n'est qu'indirectement un Fix, on ne garde
  en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
  source d'incompatibilité.

- Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement

- Plus de "Require Prolog" (intégré par défaut)

Outils

- deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; 
  coqtop est un lien vers le plus efficace possible (coqtop.opt s'il existe,
  coqtop.byte sinon); -full maintenant obsolete

- do_Makefile s'appelle maintenant coq_makefile

Utilisation générale

- La plupart des erreurs de typage sont maintenant localisée dans le
  source (à l'exception des erreurs d'univers et de garde).

- Rapidité accrue

Développeurs

- Beaucoup de modification dans le sens de la simplification et de la
  documentation (mais cela reste une version de transition)