diff options
author | 2000-12-22 09:11:06 +0000 | |
---|---|---|
committer | 2000-12-22 09:11:06 +0000 | |
commit | 6fa6f0f6e8da7eb0cfe393e4b8853e1488fa5b3f (patch) | |
tree | 32262e2560f3d4afe59169b79f38ae53653af72a /CHANGES | |
parent | c662ae83d2b7484ecdc0f4c49c3ce22c854ec587 (diff) |
Traduction en francais de 'CHANGES' dont le contenu était en français
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 178 |
1 files changed, 0 insertions, 178 deletions
@@ -1,178 +0,0 @@ -Métathéorie - -- 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. - -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 - -- 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). - -- 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. - -- Les déclarations de constantes et de variables peuvent maintenant -être accédées par un nom long de la forme "Logic.f_equal". La -bibliothèque standard a maintenant une racine nommée "Coq". Tout nom -de la forme "Coq.Logic.f_equal" dénote ainsi un chemin absolu vers une -déclaration. - -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 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. - -- Binding of constructions in Grammar rules is now done with absolute - paths. This means overloading of syntax for different constructions - having same base name is no longer possible. - -- Syntax changes - - 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 - New: Test Implicit Arguments - -- New commands to relate physical paths to a logical paths: - Add LoadPath physical_dir as logical_dir - Add Rec LoadPath physical_dir as logical_dir - -- 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 from Yves Bertot); Search can - be restricted to some modules - -- Le point final des commandes doit être suivi d'un blanc (retour chariot, tabulation ou espace) - - -Tactiques - -- Langage de tactique Ltac - -- 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 - -- 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) - -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) |