path: root/CHANGEMENTS

EXPLIQUER le changement de Fact (JCF ??)

Langage

- Ajout de d�finitions locales (Let-In) avec la syntaxe [x:=u]t. Cela
  peut entrainer des comportements nouveaux pour certaines tactiques.

- Les d�finitions globales de la biblioth�que standard sont associ�es
  � un nom long refl�tant la structure logique de la notion. Un tel nom
  long a la forme Coq.Lists.PolyList.Map.flat_map o� Coq d�note que la
  d�finition flat_map fait partie de la biblioth�que standard, Lists
  qu'elle se trouve dans le r�pertoire Lists, PolyList qu'elle se trouve
  dans le module PolyList, et Map qu'elle se trouve dans la section Map.

- On peut (et il est conseill�) associer � un r�pertoire physique un
  nom logique dans la structure des noms de Coq. Les d�finitions de la
  biblioth�que standard sont associ�es au pr�fixe logique `Coq'. Pour
  associer un r�pertoire physique � un nom logique, il faut utiliser
  l'option -R de coqtop et coqc (cf Outils). Par d�faut, le nom logique
  "Scratch" est utilis� pour toute d�finition globale non associ�e � un
  module non associ� � un nom logique.

- Le nom long des d�finitions globales est accessible pour
  l'utilisateur par la notation point�e (style Coq.Arith.Plus.plus_assoc_l).
  La syntaxe du "." final change (cf Vernac). Le nommage des d�finitions
  globales change (cf M�tath�orie).

- Le probl�me avec les identificateurs se terminant par un nombre
  sup�rieur � 2^30 est r�solu.

- Le caract�re "$" n'est plus autoris� dans les identificateurs.

Extensions de syntaxe avec Grammar et Syntax

- L'analyseur lexical consid�re maintenant comme lex�me toute suite de
  symboles. Des exceptions ont �t� cod�es dans l'analyseur lexical pour s�parer
  des lex�mes que l'on a l'habitude de "coller" (par exemple A->~B), mais ce
  n'est pas exhaustif et des espaces doivent �tre ins�r�s dans certains cas
  qui n'ont pas �t� trait�s (source d'incompatibilit�).

- L'entr�e "command" dans "Grammar" et dans les piquants s'appelle
  maintenant "constr" comme dans "Syntax".

- 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 piqants
  <: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.

- L'interpr�tation des noms dans les r�gles de grammaire (Grammar) se
  font maintenant avec un nom long. Ceci interdit la surcharge de
  notation bas�e uniquement sur le nom court.

- 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

- Cases engendre parfois des noms differents (source th�orique
  d'incompatibilit� mais insensible dans la pratique)

- Les alias de motifs ayant un type d�pendant ne sont pour l'instant
  pas trait�s

- 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.


Commandes

- Changement de nom de certaines commandes

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

  Implicit Arguments On -> Set Implicit Arguments
  Implicit Arguments Off -> Unset Implicit Arguments

  Nouveau: Test Implicit Arguments

- End Silent �tait interpr�t� comme une fin de section 
  Begin Silent -> Set Silent
  End Silent -> Unset Silent.

- Commandes pour associer des chemins physiques � des chemins logiques

  Add LoadPath physical_dir as logical_dir
  Add Rec LoadPath physical_dir as logical_dir

- Import module (re-)rend visible toutes les d�finitions et th�or�mes
  d�finis dans module.

- D�claration manuelle des implicites avec

  "Implicits ident." pour activer les arguments implicites pour ident
  ind�pendamment de l'�tat courant du mode implicite.

  "Implicits ident [ num num ... num ]." pour donner explicitement
  quels arguments doivent �tre implicites.

- SearchPattern / SearchRewrite (contribution de Yves Bertot); Search
  peut lui aussi �tre restreint � une recherche dans ou � l'ext�rieur de
  modules.

- Le point final des commandes doit �tre suivi d'un blanc (retour
  chariot, tabulation ou espace)

- L�g�re restriction de la syntaxe de Cbv Delta : l'option [-myconst]
  de Cbv doit imm�diatement suivre Delta

- Nouveau: Debug On/Off positionne/d�branche le d�bogueur de tactiques
  (encore tr�s exp�rimental).

- Fact se comporte diff�remment (comment, JCF ??)

Tactiques

- Langage de tactiques Ltac: nouvelle couche de m�talangage pour traiter de
  petites automatisations. C'est essentiellement un petit noyau fonctionnel
  muni d'op�rateurs de filtrage �labor�s (sur les termes, les contextes de
  preuves et r�alisant du backtracking). Pour conna�tre les justifications
  d'un tel language et se procurer une documentation provisoire de Ltac, se
  r�f�rer � l'URL suivante:

      http://logical.inria.fr/~delahaye/

- Tactique Let renomm� en LetTac et utilise le let-in primitif;
  Induction renomm� en OldInduction et nouveau Induction plus
  "convivial".

- Elim avec un sch�ma d'�limination diff�rent de celui cr�� � la
  d�finition d'un inductif n'est plus possible. Il faut utiliser Elim
  <hyp> with <nom du sch�ma d'�limination>.

- 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. 
  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)

- Unfold �choue si on lui donne en argument une d�finition non d�pliable

- Tauto et Intuition ont �t� int�gralement r��crites en utilisant le nouveau
  langage de tactiques Ltac. Les cons�quences sont un gain consid�rable en
  compacit� et en performances. Tauto est totalement conservatif. Intuition
  perd l�g�rement en puissance mais gagne une s�mantique plus claire.

- AutoRewrite ne s'occupe maintenant que du but principal et c'est les
  Hint Rewrite qui g�rent les sous-buts g�n�r�s.

- Les instantiations redondantes ou incompatibles de Apply ... with ...
  sont maintenant correctement trait�es.


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 de l'option -R de coqtop et coqc pour associer un
  r�pertoire physique � un r�pertoire logique (cf M�tath�orie) 

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


D�veloppeurs

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