diff options
57 files changed, 526 insertions, 540 deletions
@@ -17,7 +17,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of are distributed under the terms of the GNU Lesser General Public License Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010, -The Coq development team, CNRS, INRIA and Université Paris Sud. +The Coq development team, CNRS, INRIA and Université Paris Sud. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -29,9 +29,9 @@ plugins/cc developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud University at Nijmegen, 2005-2008) plugins/correctness - developed by Jean-Christophe Filliâtre (LRI, 1999-2001) + developed by Jean-Christophe Filliâtre (LRI, 1999-2001) plugins/dp - developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre + developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre (LRI, 2005-2008) plugins/extraction developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now) @@ -40,25 +40,25 @@ plugins/field plugins/firstorder developed by Pierre Corbineau (LRI, 2003-2008) plugins/fourier - developed by Loïc Pottier (INRIA-Lemme, 2001) + developed by Loïc Pottier (INRIA-Lemme, 2001) plugins/funind developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008), Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) and Yves Bertot (INRIA-Marelle, 2005-2006) plugins/omega - developed by Pierre Crégut (France Telecom R&D, 1996) + developed by Pierre Crégut (France Telecom R&D, 1996) plugins/nsatz - developed by Loïc Pottier (INRIA-Marelle, 2009) + developed by Loïc Pottier (INRIA-Marelle, 2009) plugins/ring developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick Loiseleur (LRI, 1997-1999) plugins/romega - developed by Pierre Crégut (France Telecom R&D, 2001-2004) + developed by Pierre Crégut (France Telecom R&D, 2001-2004) plugins/rtauto developed by Pierre Corbineau (LRI, 2005) plugins/setoid_ring - developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), - Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) + developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), + Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) and Bruno Barras (INRIA LogiCal, 2005-2006), plugins/subtac developed by Matthieu Sozeau (LRI, 2005-2008) @@ -67,18 +67,18 @@ plugins/xml as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as part of the ProofWeb project (Radboud University at Nijmegen, 2008) plugins/micromega - developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some + developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and interface to the csdp solver uses code from John Harrison (University of Cambridge, 1998) parsing/search.ml mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004) theories/ZArith - started by Pierre Crégut (France Telecom R&D, 1996) + started by Pierre Crégut (France Telecom R&D, 1996) theories/Strings - developed by Laurent Théry (INRIA-Lemme, 2003) + developed by Laurent Théry (INRIA-Lemme, 2003) theories/Numbers/Cyclic - developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008) + developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008) ide/utils some files come from Maxence Guesdon's Cameleon tool @@ -87,16 +87,16 @@ development influenced the design of Coq especially with C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi, - C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas, - P.-Y. Strub, L. Théry, B. Werner + C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas, + P.-Y. Strub, L. Théry, B. Werner The development of Coq also significantly benefited from feedback, suggestions or short contributions from: - C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D), - P. Castéran (University Bordeaux 1), + C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D), + P. Castéran (University Bordeaux 1), the Foundations Group (Radboud University, Nijmegen, The Netherlands), - Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), + Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), F. Garillot, G. Gonthier (INRIA-MSR joint lab), INRIA-Gallium project, the CS dept at Yale, the CIS dept at U. Penn, @@ -117,34 +117,34 @@ of the Coq Proof assistant during the indicated time: Olivier Desmettre (INRIA, 2001-2003) Gilles Dowek (INRIA, 1991-1994) Amy Felty (INRIA, 1993) - Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now) - Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) - Stéphane Glondu (INRIA-PPS, 2007-now) - Benjamin Grégoire (INRIA, 2003-now) + Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now) + Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) + Stéphane Glondu (INRIA-PPS, 2007-now) + Benjamin Grégoire (INRIA, 2003-now) Hugo Herbelin (INRIA, 1996-now) - Gérard Huet (INRIA, 1985-1997) + Gérard Huet (INRIA, 1985-1997) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now) Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) - Claude Marché (INRIA 2003-2004 & LRI, 2004) + Claude Marché (INRIA 2003-2004 & LRI, 2004) Benjamin Monate (LRI, 2003) - César Muñoz (INRIA, 1994-1995) + César Muñoz (INRIA, 1994-1995) Chetan Murthy (INRIA, 1992-1994) Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now) Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-now) - Pierre-Marie Pédrot (INRIA-PPS, 2011-now) + Pierre-Marie Pédrot (INRIA-PPS, 2011-now) Matthias Puech (INRIA-Bologna, 2008-now) - Yann Régis-Gianas (INRIA-PPS, 2009-now) - Clément Renard (INRIA, 2001-2004) + Yann Régis-Gianas (INRIA-PPS, 2009-now) + Clément Renard (INRIA, 2001-2004) Claudio Sacerdoti Coen (INRIA, 2004-2005) - Amokrane Saïbi (INRIA, 1993-1998) + Amokrane Saïbi (INRIA, 1993-1998) Vincent Siles (INRIA, 2007) - Élie Soubiran (INRIA, 2007-now) + Élie Soubiran (INRIA, 2007-now) Matthieu Sozeau (INRIA, 2005-now) Arnaud Spiwack (INRIA, 2006-now) Enrico Tassi (INRIA, 2011-now) @@ -156,9 +156,9 @@ INRIA refers to: CNRS refers to: Centre National de la Recherche Scientifique LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623 - CNRS and Université Paris-Sud + CNRS and Université Paris-Sud ENS Lyon refers to: - Ecole Normale Supérieure de Lyon -PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126, - CNRS and Université Paris 7 + Ecole Normale Supérieure de Lyon +PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126, + CNRS and Université Paris 7 **************************************************************************** @@ -25,29 +25,29 @@ Theories: Doc: -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection +- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection - Documenter le filtrage sur les types inductifs avec let-ins (dont la compatibilite V6) -- Ajouter let dans les règles du CIC +- Ajouter let dans les règles du CIC -> FAIT, mais reste a documenter le let dans les inductifs et les champs manifestes dans les Record - revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) +- faut-il mieux spécifier la sémantique de Simpl (??) -- Préciser la clarification syntaxique de IntroPattern +- Préciser la clarification syntaxique de IntroPattern - preciser que Goal vient en dernier dans une clause pattern list et qu'il doit apparaitre si il y a un "in" - Omega Time debranche mais Omega System et Omega Action remarchent ? - Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter +- Syntaxe Conditional tac Rewrite marche, à documenter - Documenter Dependent Rewrite et CutRewrite ? - Ajouter les motifs sous-termes de ltac - ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) +- mettre à jour la doc de induction (arguments multiples) (Pierre C.) +- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) +--> mettre à jour le CHANGES (vers la ligne 72) @@ -3,16 +3,16 @@ - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml o arguments implicites - - les calculer une fois pour toutes à la déclaration (dans Declare) + - les calculer une fois pour toutes à la déclaration (dans Declare) et stocker cette information dans le in_variable, in_constant, etc. - o Environnements compilés (type Environ.compiled_env) - - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) + o Environnements compilés (type Environ.compiled_env) + - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) - o Efficacité - - utiliser DOPL plutôt que DOPN (sauf pour Case) + o Efficacité + - utiliser DOPL plutôt que DOPN (sauf pour Case) - batch mode => pas de undo, ni de reset - - conversion : déplier la constante la plus récente + - conversion : déplier la constante la plus récente - un cache pour type_of_const, type_of_inductive, type_of_constructor, lookup_mind_specif diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d872110b9..2f62be9af 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -615,14 +615,14 @@ Changements d'organisation / modules : Std, More_util -> lib/util.ml Names -> kernel/names.ml et kernel/sign.ml - (les parties noms et signatures ont été séparées) + (les parties noms et signatures ont été séparées) - Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) + Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) Mhb -> Bij - Generic est intégré à Term (et un petit peu à Closure) + Generic est intégré à Term (et un petit peu à Closure) -Changements dans les types de données : +Changements dans les types de données : --------------------------------------- dans Generic: free_rels : constr -> int Listset.t devient : constr -> Intset.t @@ -642,7 +642,7 @@ ATTENTION: try . .. with UserError _ -> ... - mais écrire à la place + mais écrire à la place try ... with e when Logic.catchable_exception e -> ... @@ -774,7 +774,7 @@ Changements dans les inductifs Nouveaux types "constructor" et "inductive" dans Term La plupart des fonctions de typage des inductives prennent maintenant un inductive au lieu d'un oonstr comme argument. Les seules fonctions -à traduire un constr en inductive sont les find_rectype and co. +à traduire un constr en inductive sont les find_rectype and co. Changements dans les grammaires ------------------------------- @@ -782,9 +782,9 @@ Changements dans les grammaires . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex . attention : LIDENT -> IDENT (les identificateurs n'ont pas de - casse particulière dans Coq) + casse particulière dans Coq) - . Le mot "command" est remplacé par "constr" dans les noms de + . Le mot "command" est remplacé par "constr" dans les noms de fichiers, noms de modules et non-terminaux relatifs au parsing des termes; aussi les changements suivants "COMMAND"/"CONSTR" dans g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml* @@ -792,22 +792,22 @@ Changements dans les grammaires . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n passent en minuscule Identifier, Constr, ... - . Plusieurs parsers ont changé de format (ex: sortarg) + . Plusieurs parsers ont changé de format (ex: sortarg) Changements dans le pretty-printing ----------------------------------- - . Découplage de la traduction de constr -> rawconstr (dans detyping) + . Découplage de la traduction de constr -> rawconstr (dans detyping) et de rawconstr -> ast (dans termast) - . Déplacement des options d'affichage de printer vers termast - . Déplacement des réaiguillage d'univers du pp de printer vers esyntax + . Déplacement des options d'affichage de printer vers termast + . Déplacement des réaiguillage d'univers du pp de printer vers esyntax Changements divers ------------------ . il n'y a plus de script coqtop => coqtop et coqtop.byte sont - directement le résultat du link du code + directement le résultat du link du code => debuggage et profiling directs . il n'y a plus d'installation locale dans bin/$ARCH diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt index eb4d26591..075496db7 100644 --- a/dev/doc/extensions.txt +++ b/dev/doc/extensions.txt @@ -1,19 +1,19 @@ -Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ? +Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ? ====================================================================== -Exemple de l'ajout de l'entrée "clause": +Exemple de l'ajout de l'entrée "clause": - ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les wit_, rawwit_, et globwit_ correspondants -- ajouter partout où Genarg.argument_type est filtré le cas traitant de +- ajouter partout où Genarg.argument_type est filtré le cas traitant de ce nouveau ClauseArgType -- utiliser le rawwit_clause pour définir une entrée clause du bon +- utiliser le rawwit_clause pour définir une entrée clause du bon type et du bon nom dans le module Tactic de pcoq.ml4 -- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il +- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il faut rejouter clause dans le GLOBAL du GEXTEND -- seulement après, le nom clause sera accessible dans les TACTIC EXTEND ! +- seulement après, le nom clause sera accessible dans les TACTIC EXTEND ! diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index e7c8975bd..349164948 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -1,6 +1,6 @@ \documentclass[a4paper]{article} \usepackage{fullpage} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{amsfonts} @@ -299,7 +299,7 @@ element {\zero} and multiplicative binary operator (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for \texttt{NZ}). - Remark: The French school says ``integrité''. + Remark: The French school says ``integrité''. \itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element zero in D}{Dop\_nilpotent} {forall x, op x x = zero} diff --git a/dev/doc/newsyntax.tex b/dev/doc/newsyntax.tex index 96e61292f..d1986fa0d 100644 --- a/dev/doc/newsyntax.tex +++ b/dev/doc/newsyntax.tex @@ -5,7 +5,7 @@ \usepackage{verbatim} \usepackage[T1]{fontenc} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[french]{babel} \usepackage{amsmath} \usepackage{amssymb} @@ -15,7 +15,7 @@ \author{B.~Barras} \title{Proposition de syntaxe pour Coq} -%% Le _ est un caractère normal +%% Le _ est un caractère normal \catcode`\_=13 \let\subscr=_ \def_{\ifmmode\sb\else\subscr\fi} @@ -47,21 +47,21 @@ \section{Grammaire des tactiques} \label{tacticsyntax} -La réflexion de la rénovation de la syntaxe des tactiques n'est pas -encore aussi poussée que pour les termes (section~\ref{constrsyntax}), -mais cette section vise à énoncer les quelques principes que l'on +La réflexion de la rénovation de la syntaxe des tactiques n'est pas +encore aussi poussée que pour les termes (section~\ref{constrsyntax}), +mais cette section vise à énoncer les quelques principes que l'on souhaite suivre. \begin{itemize} -\item Réutiliser les mots-clés de la syntaxe des termes (i.e. en +\item Réutiliser les mots-clés de la syntaxe des termes (i.e. en minuscules) pour les constructions similaires de tactiques (let_in, - match, and, etc.). Le connecteur logique \texttt{and} n'étant que - rarement utilisé autrement que sous la forme \texttt{$\wedge$} (sauf - dans le code ML), on pourrait dégager ce mot-clé. -\item Les arguments passés aux tactiques sont principalement des - termes, on préconise l'utilisation d'un symbole spécial (par exemple + match, and, etc.). Le connecteur logique \texttt{and} n'étant que + rarement utilisé autrement que sous la forme \texttt{$\wedge$} (sauf + dans le code ML), on pourrait dégager ce mot-clé. +\item Les arguments passés aux tactiques sont principalement des + termes, on préconise l'utilisation d'un symbole spécial (par exemple l'apostrophe) pour passer une tactique ou une expression - (AST). L'idée étant que l'on écrit plus souvent des tactiques + (AST). L'idée étant que l'on écrit plus souvent des tactiques prenant des termes en argument que des tacticals. \end{itemize} @@ -97,15 +97,15 @@ souhaite suivre. \subsection{Arguments de tactiques} La syntaxe actuelle des arguments de tactiques est que l'on parse par -défaut une expression de tactique, ou bien l'on parse un terme si -celui-ci est préfixé par \TERM{'} (sauf dans le cas des -variables). Cela est gênant pour les utilisateurs qui doivent écrire +défaut une expression de tactique, ou bien l'on parse un terme si +celui-ci est préfixé par \TERM{'} (sauf dans le cas des +variables). Cela est gênant pour les utilisateurs qui doivent écrire des \TERM{'} pour leurs tactiques. -À mon avis, il n'est pas souhaitable pour l'utilisateur de l'obliger à -marquer une différence entre les tactiques ``primitives'' (en fait -``système'') et les tactiques définies par Ltac. En effet, on se -dirige inévitablement vers une situation où il existera des librairies +À mon avis, il n'est pas souhaitable pour l'utilisateur de l'obliger à +marquer une différence entre les tactiques ``primitives'' (en fait +``système'') et les tactiques définies par Ltac. En effet, on se +dirige inévitablement vers une situation où il existera des librairies de tactiques et il va devenir difficile de savoir facilement s'il faut ou non mettre des \TERM{'}. @@ -113,33 +113,33 @@ ou non mettre des \TERM{'}. \subsection{Bindings} -Dans un premier temps, les ``bindings'' sont toujours considérés comme -une construction du langage des tactiques, mais il est intéressant de -prévoir l'extension de ce procédé aux termes, puisqu'il s'agit +Dans un premier temps, les ``bindings'' sont toujours considérés comme +une construction du langage des tactiques, mais il est intéressant de +prévoir l'extension de ce procédé aux termes, puisqu'il s'agit simplement de construire un n{\oe}ud d'application dans lequel on -donne les arguments par nom ou par position, les autres restant à -inférer. Le principal point est de trouver comment combiner de manière -uniforme ce procédé avec les arguments implicites. +donne les arguments par nom ou par position, les autres restant à +inférer. Le principal point est de trouver comment combiner de manière +uniforme ce procédé avec les arguments implicites. -Il est toutefois important de réfléchir dès maintenant à une syntaxe -pour éviter de rechanger encore la syntaxe. +Il est toutefois important de réfléchir dès maintenant à une syntaxe +pour éviter de rechanger encore la syntaxe. -Intégrer la notation \TERM{with} aux termes peut poser des problèmes -puisque ce mot-clé est utilisé pour le filtrage: comment parser (en +Intégrer la notation \TERM{with} aux termes peut poser des problèmes +puisque ce mot-clé est utilisé pour le filtrage: comment parser (en LL(1)) l'expression: \begin{verbatim} Cases x with y ... \end{verbatim} -Soit on trouve un autre mot-clé, soit on joue avec les niveaus de -priorité en obligeant a parenthéser le \TERM{with} des ``bindings'': +Soit on trouve un autre mot-clé, soit on joue avec les niveaus de +priorité en obligeant a parenthéser le \TERM{with} des ``bindings'': \begin{verbatim} Cases (x with y) with (C z) => ... \end{verbatim} -ce qui introduit un constructeur moralement équivalent à une -application situé à une priorité totalement différente (les +ce qui introduit un constructeur moralement équivalent à une +application situé à une priorité totalement différente (les ``bindings'' seraient au plus haut niveau alors que l'application est -à un niveau bas). +à un niveau bas). \begin{figure} @@ -156,9 +156,9 @@ application situé à une priorité totalement différente (les \subsection{Enregistrements} -Il faudrait aménager la syntaxe des enregistrements dans l'optique -d'avoir des enregistrements anonymes (termes de première classe), même -si pour l'instant, on ne dispose que d'enregistrements définis a +Il faudrait aménager la syntaxe des enregistrements dans l'optique +d'avoir des enregistrements anonymes (termes de première classe), même +si pour l'instant, on ne dispose que d'enregistrements définis a toplevel. Exemple de syntaxe pour les types d'enregistrements: @@ -179,22 +179,22 @@ Exemple de syntaxe pour le constructeur: ... } \end{verbatim} -Quant aux dépendences, une convention pourrait être de considérer les -champs non annotés par le type comme non dépendants. +Quant aux dépendences, une convention pourrait être de considérer les +champs non annotés par le type comme non dépendants. Plusieurs interrogations: \begin{itemize} -\item l'ordre des champs doit-il être respecté ? +\item l'ordre des champs doit-il être respecté ? sinon, que faire pour les champs sans projection ? \item autorise-t-on \texttt{v1} a mentionner \texttt{x1} (comme dans - la définition d'un module), ce qui se comporterait comme si on avait - écrit \texttt{v1} à la place. Cela pourrait être une autre manière - de déclarer les dépendences + la définition d'un module), ce qui se comporterait comme si on avait + écrit \texttt{v1} à la place. Cela pourrait être une autre manière + de déclarer les dépendences \end{itemize} -La notation pointée pour les projections pose un problème de parsing, +La notation pointée pour les projections pose un problème de parsing, sauf si l'on a une convention lexicale qui discrimine les noms de -modules des projections et identificateurs: \texttt{x.y.z} peut être +modules des projections et identificateurs: \texttt{x.y.z} peut être compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}. @@ -204,17 +204,17 @@ compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}. \subsection{Quelques principes} \begin{enumerate} -\item Diminuer le nombre de niveaux de priorité en regroupant les - règles qui se ressemblent: infixes, préfixes, lieurs (constructions - ouvertes à droite), etc. -\item Éviter de surcharger la signification d'un symbole (ex: - \verb+( )+ comme parenthésage et produit dans la V7). +\item Diminuer le nombre de niveaux de priorité en regroupant les + règles qui se ressemblent: infixes, préfixes, lieurs (constructions + ouvertes à droite), etc. +\item Éviter de surcharger la signification d'un symbole (ex: + \verb+( )+ comme parenthésage et produit dans la V7). \item Faire en sorte que les membres gauches (motifs de Cases, lieurs d'abstraction ou de produits) utilisent une syntaxe compatible avec celle des membres droits (branches de Cases et corps de fonction). \end{enumerate} -\subsection{Présentation de la grammaire} +\subsection{Présentation de la grammaire} \begin{figure} \begin{rulebox} @@ -286,15 +286,15 @@ compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}. \label{gram-annexes} \end{figure} -La grammaire des termes (correspondant à l'état \texttt{barestate}) -est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate -par rapport aux précédentes versions de Coq d'importants changements -de priorité, le plus marquant étant celui de l'application qui se -trouve désormais juste au dessus\footnote{La convention est de -considérer les opérateurs moins lieurs comme ``au dessus'', -c'est-à-dire ayant un niveau de priorité plus élévé (comme c'est le +La grammaire des termes (correspondant à l'état \texttt{barestate}) +est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate +par rapport aux précédentes versions de Coq d'importants changements +de priorité, le plus marquant étant celui de l'application qui se +trouve désormais juste au dessus\footnote{La convention est de +considérer les opérateurs moins lieurs comme ``au dessus'', +c'est-à -dire ayant un niveau de priorité plus élévé (comme c'est le cas avec le niveau de la grammaire actuelle des termes).} des -constructions fermées à gauche et à droite. +constructions fermées à gauche et à droite. La grammaire des noms globaux est la suivante: \begin{eqnarray*} @@ -304,43 +304,43 @@ La grammaire des noms globaux est la suivante: \nlsep \NT{ident}\TERM{.}\NT{global} \end{eqnarray*} -Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont +Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont reconnues au niveau du lexer pour ne pas entrer en conflit avec le $\TERM{?}$ de l'existentielle. -Les opérateurs infixes ou préfixes sont tous au même niveau de -priorité du point de vue de Camlp4. La solution envisagée est de les -gérer à la manière de Yacc, avec une pile (voir discussions plus +Les opérateurs infixes ou préfixes sont tous au même niveau de +priorité du point de vue de Camlp4. La solution envisagée est de les +gérer à la manière de Yacc, avec une pile (voir discussions plus bas). Ainsi, l'implication est un infixe normal; la quantification -universelle et le let sont vus comme des opérateurs préfixes avec un -niveau de priorité plus haut (i.e. moins lieur). Il subsiste des -problèmes si l'on ne veut pas écrire de parenthèses dans: +universelle et le let sont vus comme des opérateurs préfixes avec un +niveau de priorité plus haut (i.e. moins lieur). Il subsiste des +problèmes si l'on ne veut pas écrire de parenthèses dans: \begin{verbatim} A -> (!x. B -> (let y = C in D)) \end{verbatim} -La solution proposée est d'analyser le membre droit d'un infixe de -manière à autoriser les préfixes et les infixes de niveau inférieur, -et d'exiger le parenthésage que pour les infixes de niveau supérieurs. +La solution proposée est d'analyser le membre droit d'un infixe de +manière à autoriser les préfixes et les infixes de niveau inférieur, +et d'exiger le parenthésage que pour les infixes de niveau supérieurs. -En revanche, à l'affichage, certains membres droits seront plus +En revanche, à l'affichage, certains membres droits seront plus lisibles s'ils n'utilisent pas cette astuce: \begin{verbatim} (fun x => x) = fun x => x \end{verbatim} -La proposition est d'autoriser ce type d'écritures au parsing, mais -l'afficheur écrit de manière standardisée en mettant quelques -parenthèses superflues: $\TERM{=}$ serait symétrique alors que -$\rightarrow$ appellerait l'afficheur de priorité élevée pour son +La proposition est d'autoriser ce type d'écritures au parsing, mais +l'afficheur écrit de manière standardisée en mettant quelques +parenthèses superflues: $\TERM{=}$ serait symétrique alors que +$\rightarrow$ appellerait l'afficheur de priorité élevée pour son sous-terme droit. -Les priorités des opérateurs primitifs sont les suivantes (le signe -$*$ signifie que pour le membre droit les opérateurs préfixes seront -affichés sans parenthèses quel que soit leur priorité): +Les priorités des opérateurs primitifs sont les suivantes (le signe +$*$ signifie que pour le membre droit les opérateurs préfixes seront +affichés sans parenthèses quel que soit leur priorité): $$ \begin{array}{c|l} -$symbole$ & $priorité$ \\ +$symbole$ & $priorité$ \\ \hline \TERM{!} & 200\,R* \\ \TERM{fun} & 200\,R* \\ @@ -351,39 +351,39 @@ $symbole$ & $priorité$ \\ \end{array} $$ -Il y a deux points d'entrée pour les termes: $\NT{constr}$ et -$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi -d'un séparateur particulier. Dans le cas où l'on veut une liste de -termes séparés par un espace, il faut lire des $\NT{simple-constr}$. +Il y a deux points d'entrée pour les termes: $\NT{constr}$ et +$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi +d'un séparateur particulier. Dans le cas où l'on veut une liste de +termes séparés par un espace, il faut lire des $\NT{simple-constr}$. Les constructions $\TERM{fix}$ et $\TERM{cofix}$ (voir aussi -figure~\ref{gram-fix}) sont fermées par end pour simplifier -l'analyse. Sinon, une expression de point fixe peut être suivie par un -\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le +figure~\ref{gram-fix}) sont fermées par end pour simplifier +l'analyse. Sinon, une expression de point fixe peut être suivie par un +\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le ``dangling else'': dans \begin{verbatim} fix f1 x {x} = fix f2 y {y} = ... and ... in ... \end{verbatim} -il faut définir une stratégie pour associer le \TERM{and} et le +il faut définir une stratégie pour associer le \TERM{and} et le \TERM{in} au bon point fixe. Un autre avantage est de faire apparaitre que le \TERM{fix} est un -constructeur de terme de première classe et pas un lieur: +constructeur de terme de première classe et pas un lieur: \begin{verbatim} fix f1 ... and f2 ... in f1 end x \end{verbatim} -Les propositions précédentes laissaient \texttt{f1} et \texttt{x} -accolés, ce qui est source de confusion lorsque l'on fait par exemple +Les propositions précédentes laissaient \texttt{f1} et \texttt{x} +accolés, ce qui est source de confusion lorsque l'on fait par exemple \texttt{Pattern (f1 x)}. Les corps de points fixes et co-points fixes sont identiques, bien que -ces derniers n'aient pas d'information de décroissance. Cela -fonctionne puisque l'annotation est optionnelle. Cela préfigure des -cas où l'on arrive à inférer quel est l'argument qui décroit -structurellement (en particulier dans le cas où il n'y a qu'un seul +ces derniers n'aient pas d'information de décroissance. Cela +fonctionne puisque l'annotation est optionnelle. Cela préfigure des +cas où l'on arrive à inférer quel est l'argument qui décroit +structurellement (en particulier dans le cas où il n'y a qu'un seul argument). \begin{figure} @@ -412,8 +412,8 @@ argument). \label{gram-fix} \end{figure} -La construction $\TERM{Case}$ peut-être considérée comme -obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et +La construction $\TERM{Case}$ peut-être considérée comme +obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et simplement. \begin{figure} @@ -456,15 +456,15 @@ simplement. \label{gram-match} \end{figure} -De manière globale, l'introduction de définitions dans les termes se -fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au -niveau vernac. Il y avait un manque de cohérence dans la +De manière globale, l'introduction de définitions dans les termes se +fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au +niveau vernac. Il y avait un manque de cohérence dans la V6, puisque l'on utilisait $=$ pour le $\TERM{let}$ et $\!:=$ pour les points fixes et les commandes vernac. % OBSOLETE: lieurs multiples supprimes %On peut remarquer que $\NT{binder}$ est un sous-ensemble de -%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant +%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant %que lieur, {\tt a} et {\tt b} sont tous deux contraints, alors qu'en %tant que terme, seul {\tt b} l'est. Cela qui signifie que l'objectif %de rendre compatibles les membres gauches et droits est {\it presque} @@ -474,14 +474,14 @@ points fixes et les commandes vernac. \subsubsection{Infixes extensibles} -Le problème de savoir si la liste des symboles pouvant apparaître en -infixe est fixée ou extensible par l'utilisateur reste à voir. +Le problème de savoir si la liste des symboles pouvant apparaître en +infixe est fixée ou extensible par l'utilisateur reste à voir. -Notons que la solution où les symboles infixes sont des -identificateurs que l'on peut définir paraît difficilement praticable: -par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais -ternaire. Il semble plus simple de garder des déclarations infixes qui -relient un symbole infixe à un terme avec deux ``trous''. Par exemple: +Notons que la solution où les symboles infixes sont des +identificateurs que l'on peut définir paraît difficilement praticable: +par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais +ternaire. Il semble plus simple de garder des déclarations infixes qui +relient un symbole infixe à un terme avec deux ``trous''. Par exemple: $$\begin{array}{c|l} $infixe$ & $identificateur$ \\ @@ -490,33 +490,33 @@ $infixe$ & $identificateur$ \\ == & \texttt{JohnMajor.eq _ ?1 _ ?2} \end{array}$$ -La syntaxe d'une déclaration d'infixe serait par exemple: +La syntaxe d'une déclaration d'infixe serait par exemple: \begin{verbatim} Infix "=" 50 := Logic.eq _ ?1 ?2; \end{verbatim} -\subsubsection{Gestion des précédences} +\subsubsection{Gestion des précédences} -Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici) -considérer que tous les opérateurs ont la même précédence et gérer -soit même la recomposition des termes à l'aide d'une pile (comme +Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici) +considérer que tous les opérateurs ont la même précédence et gérer +soit même la recomposition des termes à l'aide d'une pile (comme Yacc). \subsection{Extensions de syntaxe} -\subsubsection{Litéraux numériques} +\subsubsection{Litéraux numériques} -La proposition est de considerer les litéraux numériques comme de -simples identificateurs. Comme il en existe une infinité, il faut un -nouveau mécanisme pour leur associer une définition. Par exemple, en -ce qui concerne \texttt{Arith}, la définition de $5$ serait +La proposition est de considerer les litéraux numériques comme de +simples identificateurs. Comme il en existe une infinité, il faut un +nouveau mécanisme pour leur associer une définition. Par exemple, en +ce qui concerne \texttt{Arith}, la définition de $5$ serait $\texttt{S}~4$. Pour \texttt{ZArith}, $5$ serait $\texttt{xI}~2$. -Comme les infixes, les constantes numériques peuvent être qualifiées +Comme les infixes, les constantes numériques peuvent être qualifiées pour indiquer dans quels module est le type que l'on veut -référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et +référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et \texttt{ZArith} en \texttt{Z}): \verb+N.5+, \verb+Z.5+. \begin{eqnarray*} @@ -539,18 +539,18 @@ $$ $$ Pour l'instant l'existentielle n'admet qu'une seule variable, ce qui -oblige à écrire des cascades de $\TERM{ex}$. +oblige à écrire des cascades de $\TERM{ex}$. -Pour parser les existentielles avec deux prédicats, on peut considérer -\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en -présence de cet infixe se transforme en \texttt{ex2}. +Pour parser les existentielles avec deux prédicats, on peut considérer +\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en +présence de cet infixe se transforme en \texttt{ex2}. \subsubsection{Nouveaux infixes} -Précédences des opérateurs infixes (les plus grands associent moins fort): +Précédences des opérateurs infixes (les plus grands associent moins fort): $$ \begin{array}{l|l|c|l} -$identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ +$identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ \hline \texttt{iff} & $Logic$ & \longleftrightarrow & 100 \\ \texttt{or} & $Logic$ & \vee & 80\, R \\ @@ -590,8 +590,8 @@ $identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ \end{array} $$ -Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci -définit deux égalités, ou alors les mettre dans des modules différents. +Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci +définit deux égalités, ou alors les mettre dans des modules différents. \subsection{Exemples} @@ -611,20 +611,20 @@ Fixpoint plus n m : nat {struct n} := \subsection{Questions ouvertes} -Voici les points sur lesquels la discussion est particulièrement +Voici les points sur lesquels la discussion est particulièrement ouverte: \begin{itemize} \item choix d'autres symboles pour les quantificateurs \TERM{!} et - \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!} + \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!} pour la qunatification universelle, mais on choisirait quelquechose - comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop - de symétrie entre ces quantificateurs (l'un est primitif, l'autre + comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop + de symétrie entre ces quantificateurs (l'un est primitif, l'autre pas). -\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc. -\item la possibilité d'introduire plusieurs variables du même type est - pour l'instant supprimée au vu des problèmes de compatibilité de - syntaxe entre les membres gauches et membres droits. L'idée étant - que l'inference de type permet d'éviter le besoin de déclarer tous +\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc. +\item la possibilité d'introduire plusieurs variables du même type est + pour l'instant supprimée au vu des problèmes de compatibilité de + syntaxe entre les membres gauches et membres droits. L'idée étant + que l'inference de type permet d'éviter le besoin de déclarer tous les types. \end{itemize} @@ -632,19 +632,19 @@ ouverte: \subsubsection{Lieur multiple} -L'écriture de types en présence de polymorphisme est souvent assez -pénible: +L'écriture de types en présence de polymorphisme est souvent assez +pénible: \begin{verbatim} Check !(A:Set) (x:A) (B:Set) (y:B). P A x B y; \end{verbatim} -On pourrait avoir des déclarations introduisant à la fois un type +On pourrait avoir des déclarations introduisant à la fois un type d'une certaine sorte et une variable de ce type: \begin{verbatim} Check !(x:A:Set) (y:B:Set). P A x B y; \end{verbatim} -Noter que l'on aurait pu écrire: +Noter que l'on aurait pu écrire: \begin{verbatim} Check !A x B y. P A (x:A:Set) B (y:B:Set); \end{verbatim} @@ -654,19 +654,19 @@ Check !A x B y. P A (x:A:Set) B (y:B:Set); \subsection{Questions diverses} Changer ``Pattern nl c ... nl c'' en ``Pattern [ nl ] c ... [ nl ] c'' -pour permettre des chiffres seuls dans la catégorie syntaxique des +pour permettre des chiffres seuls dans la catégorie syntaxique des termes. -Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ? +Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ? -Même problème pour l'entier de Specialize (ou virer Specialize ?) ? +Même problème pour l'entier de Specialize (ou virer Specialize ?) ? \subsection{Questions en suspens} -\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur -et en profondeur ? Quelle recherche par défaut ? +\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur +et en profondeur ? Quelle recherche par défaut ? -\section*{Remarques pêle-mêle (HH)} +\section*{Remarques pêle-mêle (HH)} Autoriser la syntaxe @@ -685,16 +685,16 @@ Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ?? \begin{itemize} -\item Mettre \verb=/= et * au même niveau dans R. +\item Mettre \verb=/= et * au même niveau dans R. -\item Changer la précédence du - unaire dans R. +\item Changer la précédence du - unaire dans R. \item Ajouter Require Arith par necessite si Require ArithRing ou Require ZArithRing. \item Ajouter Require ZArith par necessite si Require ZArithRing ou Require Omega. -\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et -l'ajouter à côté des Require Ring. +\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et +l'ajouter à côté des Require Ring. \item Remplacer "Check n" par "n:Check ..." diff --git a/dev/doc/style.txt b/dev/doc/style.txt index a8924ba65..27695a09b 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,16 +1,16 @@ -<< L'uniformité du style est plus importante que le style lui-même. >> +<< L'uniformité du style est plus importante que le style lui-même. >> (Kernigan & Pike, The Practice of Programming) Mode Emacs ========== Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - avec le réglage suivant : (setq tuareg-in-indent 2) + avec le réglage suivant : (setq tuareg-in-indent 2) -Types récursifs et filtrages +Types récursifs et filtrages ============================ - Une barre de séparation y compris sur le premier constructeur + Une barre de séparation y compris sur le premier constructeur type t = | A @@ -20,9 +20,9 @@ match expr with | A -> ... | B x -> ... -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le +Remarque : à partir de la 8.2 environ, la tendance est à utiliser le format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : +produisant un aspect visuel intéressant de bloc : type t = | A @@ -40,11 +40,11 @@ let f expr = function | A -> ... | B x -> ... -Le deuxième cas est obtenu sous tuareg avec les réglages +Le deuxième cas est obtenu sous tuareg avec les réglages (setq tuareg-with-indent 0) (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien + (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien /// pour les let mais pas pour les let-in Conditionnelles @@ -55,7 +55,7 @@ Conditionnelles deuxieme-cas Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. + parenthèses i.e. if condition then begin instr1; @@ -65,7 +65,7 @@ Conditionnelles instr4 end - Si la première branche lève une exception, évitez le else i.e. + Si la première branche lève une exception, évitez le else i.e. if condition then if condition then error "machin"; error "machin" -----> suite diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 175297f91..9892a4419 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -1,6 +1,6 @@ \documentclass[a4paper]{book} \usepackage{fullpage} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{amsfonts} @@ -245,7 +245,7 @@ Coq V6.3.1& released 7 December 1999\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\ +Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\ & & \feature{kernel-centric} architecture \\ & & more care for outside readers\\ & & (indentation, ocaml warning protection)\\ diff --git a/doc/LICENSE b/doc/LICENSE index 990874803..ada22e669 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -8,7 +8,7 @@ forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. -The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine +The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine Paulin-Mohring. All documents (the LaTeX source and the PostScript, PDF and html outputs) are copyright (c) INRIA 1999-2006. The material connected to the Coq Tutorial may be distributed only subject to the @@ -25,7 +25,7 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo +The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All documents (the LaTeX source and the PostScript, PDF and html outputs) are copyright (c) INRIA 2004-2006. The material connected to the FAQ @@ -36,7 +36,7 @@ http://www.opencontent.org/openpub/). Options A and B are *not* elected. The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre -Castéran and Eduardo Gimenez. All related documents (the LaTeX and +Castéran and Eduardo Gimenez. All related documents (the LaTeX and BibTeX sources and the PostScript, PDF and html outputs) are copyright (c) INRIA 1997-2006. The material connected to the Tutorial on [Co-]Inductive Types in Coq may be distributed only subject to the diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index 0d727e170..d0884be0d 100644 --- a/doc/RecTutorial/RecTutorial.tex +++ b/doc/RecTutorial/RecTutorial.tex @@ -19,7 +19,7 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}} % \newcommand{\refmancite}[1]{\cite{coqrefman}} % \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{makeidx} % \usepackage{multind} @@ -1007,7 +1007,7 @@ The following commented examples will show the different situations to consider. %q_r\;({c}_i\;x_1\;\ldots x_n)$$ for dependent one. In the %following section, we illustrate this general scheme for different %recursive types. -%%\textbf{A vérifier} +%%\textbf{A vérifier} \subsubsection{The Empty Type} @@ -1505,7 +1505,7 @@ definition of the notions of \emph{positivity condition} and %arguments of its own introduction rules, in the sense on the following %definition: -%\textbf{La définition du manuel de référence est plus complexe: +%\textbf{La définition du manuel de référence est plus complexe: %la recopier ou donner seulement des exemples? %} %\begin{enumerate} @@ -1718,7 +1718,7 @@ Inductive ex_Prop (P : Prop {\arrow} Prop) : Prop := %*) %\end{alltt} -% \textbf{Et par ça? +% \textbf{Et par ça? %} Notice that predicativity on sort \citecoq{Set} forbids us to build @@ -2300,8 +2300,8 @@ Qed. \begin{exercise} Consider the following language of arithmetic expression, and its operational semantics, described by a set of rewriting rules. -%\textbf{J'ai enlevé une règle de commutativité de l'addition qui -%me paraissait bizarre du point de vue de la sémantique opérationnelle} +%\textbf{J'ai enlevé une règle de commutativité de l'addition qui +%me paraissait bizarre du point de vue de la sémantique opérationnelle} \begin{alltt} Inductive ArithExp : Set := @@ -3150,7 +3150,7 @@ Qed. It is interesting to look at another proof of \citecoq{vector0\_is\_vnil}, which illustrates a technique developed and used by various people (consult in the \emph{Coq-club} mailing -list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Théry, +list archive the contributions by Yves Bertot, Pierre Letouzey, Laurent Théry, Jean Duprat, and Nicolas Magaud, Venanzio Capretta and Conor McBride). This technique is also used for unfolding infinite list definitions (see chapter13 of~\cite{coqart}). diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex index 6fb7534d5..2a2c21196 100644 --- a/doc/RecTutorial/coqartmacros.tex +++ b/doc/RecTutorial/coqartmacros.tex @@ -46,8 +46,8 @@ \renewcommand{\marginpar}[1]{} \addtocounter{secnumdepth}{1} -\providecommand{\og}{«} -\providecommand{\fg}{»} +\providecommand{\og}{«} +\providecommand{\fg}{»} \newcommand{\hard}{\mbox{\small *}} diff --git a/doc/RecTutorial/manbiblio.bib b/doc/RecTutorial/manbiblio.bib index 26064e864..caee81782 100644 --- a/doc/RecTutorial/manbiblio.bib +++ b/doc/RecTutorial/manbiblio.bib @@ -4,11 +4,11 @@ @TECHREPORT{RefManCoq, AUTHOR = {Bruno~Barras, Samuel~Boutin, - Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye, - Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez, - Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz, + Cristina~Cornes, Judicaël~Courant, Yann~Coscoy, David~Delahaye, + Daniel~de~Rauglaudre, Jean-Christophe~Filliâtre, Eduardo~Giménez, + Hugo~Herbelin, Gérard~Huet, Henri~Laulhère, César~Muñoz, Chetan~Murthy, Catherine~Parent-Vigouroux, Patrick~Loiseleur, - Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner}, + Christine~Paulin-Mohring, Amokrane~Saïbi, Benjamin~Werner}, INSTITUTION = {INRIA}, TITLE = {{The Coq Proof Assistant Reference Manual -- Version V6.2}}, YEAR = {1998} @@ -461,9 +461,9 @@ of the {ML} language}, title = {The {Coq} Proof Assistant - A tutorial, Version 6.1}, institution = {INRIA}, type = {rapport technique}, - month = {Août}, + month = {Août}, year = {1997}, - note = {Version révisée distribuée avec {Coq}}, + note = {Version révisée distribuée avec {Coq}}, number = {204}, } diff --git a/doc/RecTutorial/morebib.bib b/doc/RecTutorial/morebib.bib index 11dde2cd5..438f2133d 100644 --- a/doc/RecTutorial/morebib.bib +++ b/doc/RecTutorial/morebib.bib @@ -1,14 +1,14 @@ @book{coqart, title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions", - author = "Yves Bertot and Pierre Castéran", + author = {Yves Bertot and Pierre Castéran}, publisher = "Springer Verlag", series = "Texts in Theoretical Computer Science. An EATCS series", year = 2004 } @Article{Coquand:Huet, - author = {Thierry Coquand and Gérard Huet}, + author = {Thierry Coquand and Gérard Huet}, title = {The Calculus of Constructions}, journal = {Information and Computation}, year = {1988}, diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 647a151d7..5a6691072 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -14,7 +14,7 @@ %\usepackage{multicol} \usepackage{hevea} \usepackage{fullpage} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[english]{babel} \ifpdf % si on est en pdflatex @@ -138,7 +138,7 @@ \large(\protect\ref{lastquestion} \ Hints) } -\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux} +\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux} \maketitle %%%%%%% @@ -254,7 +254,7 @@ notes~\cite{Types:Dowek}. \item[Inductive types] Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}. \item[Co-Inductive types] -Eduardo Giménez' thesis~\cite{EGThese}. +Eduardo Giménez' thesis~\cite{EGThese}. \item[Miscellaneous] A \ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq \end{description} @@ -397,7 +397,7 @@ New versions of {\Coq} are announced on the coq-club mailing list. If you only w \Question{Is there any book about {\Coq}?} -The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004: +The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004: \begin{quote} ``This book provides a pragmatic introduction to the development of proofs and certified programs using \Coq. With its large collection of @@ -1124,7 +1124,7 @@ Qed. Just use the semi-decision tactic: \firstorder. \iffalse -todo: demander un exemple à Pierre +todo: demander un exemple à Pierre \fi \Question{My goal is solvable by a sequence of rewrites, how can I prove it?} @@ -1200,7 +1200,7 @@ Qed. \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?} -You need the {\gb} tactic (see Loïc Pottier's homepage). +You need the {\gb} tactic (see Loïc Pottier's homepage). \subsection{Tactics usage} @@ -1265,7 +1265,7 @@ You can split your hint bases into smaller ones. \Question{What is the equivalent of {\tauto} for classical logic?} -Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation. +Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation. \Question{I want to replace some term with another in the goal, how can I do it?} @@ -1914,7 +1914,7 @@ Notation "x ^2" := (Rmult x x) (at level 20). \end{verbatim} Note that you can not use: \begin{tt} -Notation "x $^²$" := (Rmult x x) (at level 20). +Notation "x $^2$" := (Rmult x x) (at level 20). \end{tt} because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8. diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib index d41ab7f09..4d90efcdb 100644 --- a/doc/faq/fk.bib +++ b/doc/faq/fk.bib @@ -16,11 +16,11 @@ } @PHDTHESIS{EGThese, - author = {Eduardo Giménez}, + author = {Eduardo Giménez}, title = {Un Calcul de Constructions Infinies et son application -a la vérification de systèmes communicants}, - type = {thèse d'Université}, - school = {Ecole Normale Supérieure de Lyon}, +a la vérification de systèmes communicants}, + type = {thèse d'Université}, + school = {Ecole Normale Supérieure de Lyon}, month = {December}, year = {1996}, } @@ -29,7 +29,7 @@ a la vérification de systèmes communicants}, %%%%%%% Semantique %%%%%%% @misc{Sem:cours, - author = "François Pottier", + author = "François Pottier", title = "{Typage et Programmation}", year = "2002", howpublished = "Lecture notes", @@ -109,7 +109,7 @@ year = {1981} @book{Coq:coqart, title = "Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions", - author = "Yves Bertot and Pierre Castéran", + author = "Yves Bertot and Pierre Castéran", publisher = "Springer Verlag", series = "Texts in Theoretical Computer Science. An EATCS series", @@ -118,8 +118,8 @@ year = {1981} @phdthesis{Coq:Del01, AUTHOR = "David Delahaye", - TITLE = "Conception de langages pour décrire les preuves et les - automatisations dans les outils d'aide à la preuve", + TITLE = "Conception de langages pour décrire les preuves et les + automatisations dans les outils d'aide à la preuve", SCHOOL = {Universit\'e Paris~6}, YEAR = "2001", Type = {Th\`ese de Doctorat} @@ -133,7 +133,7 @@ year = {1981} url = "citeseer.nj.nec.com/gimenez98tutorial.html" } @phdthesis{Coq:Mun97, - AUTHOR = "César Mu{\~{n}}oz", + AUTHOR = "César Mu{\~{n}}oz", TITLE = "Un calcul de substitutions pour la repr\'esentation de preuves partielles en th\'eorie de types", SCHOOL = {Universit\'e Paris~7}, @@ -191,7 +191,7 @@ year = {1981} } @misc{PVS-Tactics:cours, - author = "César Muñoz", + author = "César Muñoz", title = "Strategies in {PVS}", howpublished = "Lecture notes", note = "National Institute of Aerospace", @@ -288,9 +288,9 @@ year = {1981} } @TECHREPORT{modelpa2000, - AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg + AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard}, - TITLE = {Automates temporisés CALIFE}, + TITLE = {Automates temporisés CALIFE}, INSTITUTION = {Calife}, YEAR = 2000, URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz}, @@ -298,8 +298,8 @@ year = {1981} } @TECHREPORT{CaFrPaRo2000, - AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard}, - TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates}, + AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard}, + TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates}, INSTITUTION = {Calife}, YEAR = 2000, URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz}, @@ -335,7 +335,7 @@ year = {1981} MONTH = JAN, SCHOOL = {{Paris 7}}, TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, - TYPE = {Thèse d'université}, + TYPE = {Thèse d'université}, YEAR = {1989}, URL = {http://www.lri.fr/~paulin/these.ps.gz} } @@ -427,11 +427,11 @@ nd Applications}, @PHDTHESIS{Pau96b, AUTHOR = {Christine Paulin-Mohring}, - TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur}, - SCHOOL = {Université Claude Bernard Lyon I}, + TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur}, + SCHOOL = {Université Claude Bernard Lyon I}, YEAR = 1996, MONTH = DEC, - TYPE = {Habilitation à diriger les recherches}, + TYPE = {Habilitation à diriger les recherches}, URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} } @@ -488,7 +488,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, } @TECHREPORT{kmu2002rr, - AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain}, + AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain}, TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria}, INSTITUTION = {LRI}, YEAR = 2002, @@ -509,7 +509,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, } @INPROCEEDINGS{contejean03wst, - AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain}, + AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain}, TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}}, CROSSREF = {wst03}, PAGES = {71--73}, @@ -661,7 +661,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, YEAR = {2003}, EDITOR = {Albert Rubio}, MONTH = JUN, - NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain} + NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain} } @INPROCEEDINGS{FilliatreLetouzey03, @@ -740,8 +740,8 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, @INPROCEEDINGS{Filliatre01a, AUTHOR = {J.-C. Filli\^atre}, - TITLE = {La supériorité de l'ordre supérieur}, - BOOKTITLE = {Journées Francophones des Langages Applicatifs}, + TITLE = {La supériorité de l'ordre supérieur}, + BOOKTITLE = {Journées Francophones des Langages Applicatifs}, PAGES = {15--26}, MONTH = {Janvier}, YEAR = 2002, @@ -749,18 +749,18 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz}, CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps}, ABSTRACT = { - Nous présentons ici une écriture fonctionnelle de l'algorithme de + Nous présentons ici une écriture fonctionnelle de l'algorithme de Koda-Ruskey, un algorithme pour engendrer une large famille de codes de Gray. En s'inspirant de techniques de programmation par - continuation, nous aboutissons à un code de neuf lignes seulement, - bien plus élégant que les implantations purement impératives - proposées jusqu'ici, notamment par Knuth. Dans un second temps, - nous montrons comment notre code peut être légèrement modifié pour - aboutir à une version de complexité optimale. - Notre implantation en Objective Caml rivalise d'efficacité avec les - meilleurs codes C. Nous détaillons les calculs de complexité, - un exercice intéressant en présence d'ordre supérieur et d'effets de - bord combinés.} + continuation, nous aboutissons à un code de neuf lignes seulement, + bien plus élégant que les implantations purement impératives + proposées jusqu'ici, notamment par Knuth. Dans un second temps, + nous montrons comment notre code peut être légèrement modifié pour + aboutir à une version de complexité optimale. + Notre implantation en Objective Caml rivalise d'efficacité avec les + meilleurs codes C. Nous détaillons les calculs de complexité, + un exercice intéressant en présence d'ordre supérieur et d'effets de + bord combinés.} } @TECHREPORT{Filliatre00c, @@ -901,33 +901,33 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, YEAR = 1999, MONTH = {July}, URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}, - ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant - traits impératifs et fonctionnels dans le cadre de la théorie des + ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant + traits impératifs et fonctionnels dans le cadre de la théorie des types. - La théorie des types constitue un puissant langage de spécification, - naturellement adapté à la preuve de programmes purement - fonctionnels. Pour y certifier également des programmes impératifs, - nous commençons par exprimer leur sémantique de manière purement + La théorie des types constitue un puissant langage de spécification, + naturellement adapté à la preuve de programmes purement + fonctionnels. Pour y certifier également des programmes impératifs, + nous commençons par exprimer leur sémantique de manière purement fonctionnelle. Cette traduction repose sur une analyse statique des effets de bord des programmes, et sur l'utilisation de la notion de - monade, notion que nous raffinons en l'associant à la notion d'effet - de manière générale. Nous montrons que cette traduction est - sémantiquement correcte. - - Puis, à partir d'un programme annoté, nous construisons une preuve - de sa spécification, traduite de manière fonctionnelle. Cette preuve - est bâtie sur la traduction fonctionnelle précédemment - introduite. Elle est presque toujours incomplète, les parties - manquantes étant autant d'obligations de preuve qui seront laissées - à la charge de l'utilisateur. Nous montrons que la validité de ces - obligations entraîne la correction totale du programme. - - Nous avons implanté notre travail dans l'assistant de preuve - Coq, avec lequel il est dès à présent distribué. Cette - implantation se présente sous la forme d'une tactique prenant en - argument un programme annoté et engendrant les obligations de - preuve. Plusieurs algorithmes non triviaux ont été certifiés à + monade, notion que nous raffinons en l'associant à la notion d'effet + de manière générale. Nous montrons que cette traduction est + sémantiquement correcte. + + Puis, à partir d'un programme annoté, nous construisons une preuve + de sa spécification, traduite de manière fonctionnelle. Cette preuve + est bâtie sur la traduction fonctionnelle précédemment + introduite. Elle est presque toujours incomplète, les parties + manquantes étant autant d'obligations de preuve qui seront laissées + à la charge de l'utilisateur. Nous montrons que la validité de ces + obligations entraîne la correction totale du programme. + + Nous avons implanté notre travail dans l'assistant de preuve + Coq, avec lequel il est dès à présent distribué. Cette + implantation se présente sous la forme d'une tactique prenant en + argument un programme annoté et engendrant les obligations de + preuve. Plusieurs algorithmes non triviaux ont été certifiés à l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de Knuth-Morris-Pratt).} } @@ -1081,7 +1081,7 @@ tique}, } @InCollection{cc, - author = {Thierry Coquand and Gérard Huet}, + author = {Thierry Coquand and Gérard Huet}, title = {The Calculus of Constructions}, booktitle = {Information and Computation}, year = {1988}, @@ -1095,7 +1095,7 @@ tique}, title = {Inductively defined types}, booktitle = {Proceedings of Colog'88}, year = {1990}, - editor = {P. Martin-Löf and G. Mints}, + editor = {P. Martin-Löf and G. Mints}, volume = {417}, series = {LNCS}, publisher = {Springer-Verlag} @@ -1318,7 +1318,7 @@ s}, } @INPROCEEDINGS{CoHu85a, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, ADDRESS = {Linz}, BOOKTITLE = {EUROCAL'85}, PUBLISHER = SV, @@ -1329,7 +1329,7 @@ s}, } @INPROCEEDINGS{CoHu85b, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, BOOKTITLE = {Logic Colloquium'85}, EDITOR = {The Paris Logic Group}, PUBLISHER = {North-Holland}, @@ -1338,7 +1338,7 @@ s}, } @ARTICLE{CoHu86, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, JOURNAL = {Information and Computation}, NUMBER = {2/3}, TITLE = {The {Calculus of Constructions}}, @@ -2092,7 +2092,7 @@ the Calculus of Inductive Constructions}}, @PHDTHESIS{Bar99, AUTHOR = {B. Barras}, SCHOOL = {Universit\'e Paris 7}, - TITLE = {Auto-validation d'un système de preuves avec familles inductives}, + TITLE = {Auto-validation d'un système de preuves avec familles inductives}, TYPE = {Th\`ese de Doctorat}, YEAR = {1999} } @@ -2177,7 +2177,7 @@ Decomposition}}, @Book{CoqArt, - author = {Yves bertot and Pierre Castéran}, + author = {Yves bertot and Pierre Castéran}, title = {Coq'Art}, publisher = {Springer-Verlag}, year = 2004, diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex index d881329a6..ac1686c25 100644 --- a/doc/rt/RefMan-cover.tex +++ b/doc/rt/RefMan-cover.tex @@ -1,6 +1,5 @@ \documentstyle[RRcover]{book} - % L'utilisation du style `french' force le résumé français à - % apparaître en premier. + % The use of the style `french' forces the french abstract to appear first. \RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1} \RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1 @@ -26,7 +25,7 @@ Amokrane Sa{\"\i}bi, Benjamin Werner} v\'erification de preuves formelles dans une logique d'ordre sup\'erieure incluant un riche langage de d\'efinitions de fonctions. Ce document constitue le manuel de r\'ef\'erence de la version V7.1 -qui est distribu\'ee par ftp anonyme à l'adresse +qui est distribu\'ee par ftp anonyme \`a l'adresse \url{ftp://ftp.inria.fr/INRIA/coq/}} \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex index b747b812e..aefea8d42 100644 --- a/doc/rt/Tutorial-cover.tex +++ b/doc/rt/Tutorial-cover.tex @@ -1,6 +1,5 @@ \documentstyle[RRcover]{book} - % L'utilisation du style `french' force le résumé français à - % apparaître en premier. + % The use of the style `french' forces the french abstract to appear first. \RRetitle{ The Coq Proof Assistant \\ A Tutorial \\ Version 7.1 \thanks{This research was partly supported by ESPRIT Basic Research @@ -29,7 +28,7 @@ Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNR v\'erification de preuves formelles dans une logique d'ordre sup\'erieure incluant un riche langage de d\'efinitions de fonctions. Ce document constitue une introduction pratique \`a l'utilisation de -la version V7.1 qui est distribu\'ee par ftp anonyme à l'adresse +la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse \url{ftp://ftp.inria.fr/INRIA/coq/}} \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index de3d9c3f2..836944ab1 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1,6 +1,6 @@ \documentclass[11pt,a4paper]{book} \usepackage[T1]{fontenc} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage{textcomp} \usepackage{pslatex} @@ -11,7 +11,7 @@ %\makeindex \begin{document} -\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{} +\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{} %\tableofcontents @@ -30,7 +30,7 @@ manner a tutorial on the basic specification language, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools. For more advanced information, the reader could refer to the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. -Bertot and P. Castéran on practical uses of the \Coq{} system. +Bertot and P. Castéran on practical uses of the \Coq{} system. Coq can be used from a standard teletype-like shell window but preferably through the graphical user interface diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 921d3d9c9..4d0aabeb6 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -128,8 +128,8 @@ Could be one day rewritten with ocamllex/yacc to be more robust, efficient, allo open Format (* formating convention: the caller has to open the box, close it and flush the output *) (* remarks on Format: - set_margin impose un appel à set_max_indent - sprintf et bprintf sont flushées à chaque appel*) + set_margin forces a call to set_max_indent + sprintf et bprintf are flushed at each call*) (* pretty print a Raw.cp *) let rec save formatter = function diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 84bc08d2b..f9e0dc7f1 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -543,21 +543,21 @@ value coq_interprete coq_extra_args = Long_val(sp[2]); sp += 3; } else { - /* L'argument recursif est un accumulateur */ + /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction du PF partiellement appliqué */ + /* Construction of partially applied PF */ Alloc_small(accu, rec_pos + 2, Closure_tag); Field(accu, 1) = coq_env; for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; Code_val(accu) = pc; sp += rec_pos; *--sp = accu; - /* Construction de l'atom */ + /* Construction of the atom */ Alloc_small(accu, 2, ATOM_FIX_TAG); Field(accu,1) = sp[0]; Field(accu,0) = sp[1]; sp++; sp[0] = accu; - /* Construction de l'accumulateur */ + /* Construction of the accumulator */ num_args = coq_extra_args - rec_pos; Alloc_small(accu, 2+num_args, Accu_tag); Code_val(accu) = accumulate; diff --git a/kernel/constr.ml b/kernel/constr.ml index f688cca45..0fd4c9d57 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* File initially created by Gérard Huet and Thierry Coquand in 1984 *) +(* File initially created by Gérard Huet and Thierry Coquand in 1984 *) (* Extension to inductive constructions by Christine Paulin for Coq V5.6 *) (* Extension to mutual inductive constructions by Christine Paulin for Coq V5.10.2 *) @@ -15,7 +15,7 @@ (* Optimization of lifting functions by Bruno Barras, Mar 1997 *) (* Hash-consing by Bruno Barras in Feb 1998 *) (* Restructuration of Coq of the type-checking kernel by Jean-Christophe - Filliâtre, 1999 *) + Filliâtre, 1999 *) (* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *) (* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) diff --git a/lib/explore.ml b/lib/explore.ml index 90258b0e5..984114bf1 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -50,7 +50,7 @@ module Make = functor(S : SearchProblem) -> struct in explore [1] s - (*s Breadth first search. We use functional FIFOS à la Okasaki. *) + (*s Breadth first search. We use functional FIFOS à la Okasaki. *) type 'a queue = 'a list * 'a list @@ -167,7 +167,7 @@ let rewrite f p = Rem 2 : if used for an iso8859_1 encoded string, the result is wrong in very rare cases. Such a wrong case corresponds to any sequence of a character in range 192..253 immediately followed by a - character in range 128..191 (typical case in french is "déçu" which + character in range 128..191 (typical case in french is "déçu" which is counted 3 instead of 4); then no real harm to use always utf8_length even if using an iso8859_1 encoding *) diff --git a/library/nametab.ml b/library/nametab.ml index 390789852..0f7b022de 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -523,9 +523,6 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - (* Il est important de laisser le let-in, car les streams s'évaluent - paresseusement : il faut forcer l'évaluation pour capturer - l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) try str (string_of_qualid (shortest_qualid_of_global env ref)) with Not_found as e -> prerr_endline "pr_global_env not found"; raise e diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a6eefd375..07ce048ea 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -817,7 +817,7 @@ GEXTEND Gram | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> VernacAddMLPath (true, dir) - (* Pour intervenir sur les tables de paramètres *) + (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> VernacSetOption (table,v) | "Set"; table = option_table -> @@ -830,10 +830,10 @@ GEXTEND Gram | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table;field], v) - (* Un value global ci-dessous va être caché par un field au dessus! *) - (* En fait, on donne priorité aux tables secondaires *) - (* Pas de syntaxe pour les tables tertiaires pour cause de conflit *) - (* (mais de toutes façons, pas utilisées) *) + (* A global value below will be hidden by a field above! *) + (* In fact, we give priority to secondary tables *) + (* No syntax for tertiary tables due to conflict *) + (* (but they are unused anyway) *) | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table], v) diff --git a/plugins/cc/README b/plugins/cc/README index 073b140ea..c616b5daa 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -3,7 +3,7 @@ cctac: congruence-closure for coq author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan - Thèse au LRI, Université Paris Sud XI + Thèse au LRI, Université Paris Sud XI Files : diff --git a/plugins/extraction/README b/plugins/extraction/README index a9a7b04d5..458ba0deb 100644 --- a/plugins/extraction/README +++ b/plugins/extraction/README @@ -14,7 +14,7 @@ Who did it ? ------------ The current implementation (from version 7.0 up to now) has been done -by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised +by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised by C. Paulin. An earlier implementation (versions 6.x) was due to B. Werner and @@ -118,7 +118,7 @@ Axioms, and then "Extract Constant ..." [1]: -Exécution de termes de preuves: une nouvelle méthode d'extraction +Exécution de termes de preuves: une nouvelle méthode d'extraction pour le Calcul des Constructions Inductives, Pierre Letouzey, DEA thesis, 2000, http://www.pps.jussieu.fr/~letouzey/download/rapport_dea.ps.gz @@ -129,7 +129,7 @@ Types 2002 Post-Workshop Proceedings. http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz [3]: -Programmation fonctionnelle certifiée: l'extraction de programmes +Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004. http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gz http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 626629063..9e257c82a 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Méthode d'élimination de Fourier *) -(* Référence: +(* Méthode d'élimination de Fourier *) +(* Référence: Auteur(s) : Fourier, Jean-Baptiste-Joseph -Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... +Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... -Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 +Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 Pages: 326-327 @@ -20,8 +20,8 @@ http://gallica.bnf.fr/ *) (* Un peu de calcul sur les rationnels... -Les opérations rendent des rationnels normalisés, -i.e. le numérateur et le dénominateur sont premiers entre eux. +Les opérations rendent des rationnels normalisés, +i.e. le numérateur et le dénominateur sont premiers entre eux. *) type rational = {num:int; den:int} @@ -59,9 +59,9 @@ let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};; let rinf x y = x.num*y.den < y.num*x.den;; let rinfeq x y = x.num*y.den <= y.num*x.den;; -(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation +(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation c1x1+...+cnxn < d si strict=true, <= sinon, -hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. +hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. *) type ineq = {coef:rational list; @@ -70,8 +70,8 @@ type ineq = {coef:rational list; let pop x l = l:=x::(!l);; -(* sépare la liste d'inéquations s selon que leur premier coefficient est -négatif, nul ou positif. *) +(* sépare la liste d'inéquations s selon que leur premier coefficient est +négatif, nul ou positif. *) let partitionne s = let lpos=ref [] in let lneg=ref [] in @@ -85,13 +85,13 @@ let partitionne s = s; [!lneg;!lnul;!lpos] ;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) +(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): +(add_hist [(equation 1, s1);...;(équation n, sn)]) = -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; +[{équation 1, [1;0;...;0], s1}; + {équation 2, [0;1;...;0], s2}; ... - {équation n, [0;0;...;1], sn}] + {équation n, [0;0;...;1], sn}] *) let add_hist le = let n = List.length le in @@ -105,24 +105,24 @@ let add_hist le = {coef=ie;hist=(!h);strict=s}) le ;; -(* additionne deux inéquations *) +(* additionne deux inéquations *) let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; hist=List.map2 rplus ie1.hist ie2.hist; strict=ie1.strict || ie2.strict} ;; -(* multiplication d'une inéquation par un rationnel (positif) *) +(* multiplication d'une inéquation par un rationnel (positif) *) let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; hist=List.map (fun x -> rmult a x) ie.hist; strict= ie.strict} ;; -(* on enlève le premier coefficient *) +(* on enlève le premier coefficient *) let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} ;; -(* le premier coefficient: "tête" de l'inéquation *) +(* le premier coefficient: "tête" de l'inéquation *) let hd_coef ie = List.hd ie.coef ;; -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. +(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. *) let deduce_add lneg lpos = let res=ref [] in @@ -136,8 +136,8 @@ let deduce_add lneg lpos = lneg; !res ;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. +(* élimination de la première variable à partir d'une liste d'inéquations: +opération qu'on itère dans l'algorithme de Fourier. *) let deduce1 s = match (partitionne s) with @@ -146,7 +146,7 @@ let deduce1 s = (List.map ie_tl lnul)@lnew |_->assert false ;; -(* algorithme de Fourier: on élimine successivement toutes les variables. +(* algorithme de Fourier: on élimine successivement toutes les variables. *) let deduce lie = let n = List.length (fst (List.hd lie)) in @@ -157,12 +157,12 @@ let deduce lie = !lie ;; -(* donne [] si le système a des solutions, +(* donne [] si le système a des solutions, sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ +où lc est la combinaison linéaire des inéquations de départ qui donne 0 < c si s=true ou 0 <= c sinon -cette inéquation étant absurde. +cette inéquation étant absurde. *) exception Contradiction of (rational * bool * rational list) list diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4b70201b2..7274324d3 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -8,8 +8,8 @@ -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. +(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients +des inéquations et équations sont entiers. En attendant la tactique Field. *) open Term @@ -22,10 +22,10 @@ open Fourier open Contradiction (****************************************************************************** -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash +Opérations sur les combinaisons linéaires affines. +La partie homogène d'une combinaison linéaire est en fait une table de hash qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. +qui est zéro si le terme n'y est pas. *) module Constrhash = Hashtbl.Make @@ -175,9 +175,9 @@ let flin_to_alist f = !res ;; -(* Représentation des hypothèses qui sont des inéquations ou des équations. +(* Représentation des hypothèses qui sont des inéquations ou des équations. *) -type hineq={hname:constr; (* le nom de l'hypothèse *) +type hineq={hname:constr; (* le nom de l'hypothèse *) htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) hleft:constr; hright:constr; @@ -185,7 +185,7 @@ type hineq={hname:constr; (* le nom de l'hypothèse *) hstrict:bool} ;; -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 +(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 *) exception NoIneq @@ -256,12 +256,12 @@ let ineq1_of_constr (h,t) = |_-> raise NoIneq ;; -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) *) let fourier_lineq lineq1 = let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) + let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin nvar:=(!nvar)+1; @@ -342,7 +342,7 @@ let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") (****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, +Construction de la preuve en cas de succès de la méthode de Fourier, i.e. on obtient une contradiction. *) let is_int x = (x.den)=1 @@ -461,15 +461,15 @@ let mkAppL a = exception GoalDone -(* Résolution d'inéquations linéaires dans R *) +(* Résolution d'inéquations linéaires dans R *) let rec fourier () = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast concl in let fhyp=Id.of_string "new_hyp_for_fourier" in - (* si le but est une inéquation, on introduit son contraire, - et le but à prouver devient False *) + (* si le but est une inéquation, on introduit son contraire, + et le but à prouver devient False *) try match (kind_of_term goal) with App (f,args) -> @@ -497,23 +497,23 @@ let rec fourier () = |_-> raise GoalDone) |_-> raise GoalDone with GoalDone -> - (* les hypothèses *) + (* les hypothèses *) let hyps = List.map (fun (h,t)-> (mkVar h,t)) (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) with NoIneq -> ()) hyps; - (* lineq = les inéquations découlant des hypothèses *) + (* lineq = les inéquations découlant des hypothèses *) if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] then Errors.error "fourier failed" - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) + (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations + (* lc=coefficients multiplicateurs des inéquations qui donnent 0<cres ou 0<=cres selon sres *) (*print_string "Fourier's method can prove the goal...";flush stdout;*) let lutil=ref [] in @@ -523,7 +523,7 @@ let rec fourier () = then (lutil:=(h,c)::(!lutil)(*; print_rational(c);print_string " "*))) (List.combine (!lineq) lc); - (* on construit la combinaison linéaire des inéquation *) + (* on construit la combinaison linéaire des inéquation *) (match (!lutil) with (h1,c1)::lutil -> let s=ref (h1.hstrict) in @@ -603,7 +603,7 @@ let rec fourier () = (mkApp (get coq_Rinv, [|get coq_R1|])) (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) +(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 35699f219..cc89e2b9d 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -1,9 +1,9 @@ (* ========================================================================= *) (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) (* ========================================================================= *) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 235f9ce9b..f54914f25 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -2,9 +2,9 @@ (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) (* This code is the HOL LIGHT library code used by sos.ml *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) open Num diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 8566cf0d6..464bc7740 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -602,7 +602,7 @@ and pgcd_pol_rec p q x = res ) -(* Sub-résultants: +(* Sub-résultants: ai*Ai = Qi*Ai+1 + bi*Ai+2 diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index b35ef1772..6d575a541 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 83092ccc4..e425cff52 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 4e9ca6ffc..efecc8add 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (* 13/10/2002 : modified to cope with an external numbering of equations *) (* and hypothesis. Its use for Omega is not more complex and it makes *) @@ -585,15 +585,6 @@ let rec depend relie_on accu = function end | [] -> relie_on, accu -(* -let depend relie_on accu trace = - Printf.printf "Longueur de la trace initiale : %d\n" - (trace_length trace + trace_length accu); - let rel',trace' = depend relie_on accu trace in - Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace'); - rel',trace' -*) - let solve (new_eq_id,new_eq_var,print_var) system = try let _ = simplify new_eq_id false system in failwith "no contradiction" with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 3fa9e02cf..21b0f78b5 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 4ae1cb94c..af50ea0ff 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 4b6c9b790..0a99a26b3 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index f9219407e..8156e8411 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) @@ -42,8 +42,8 @@ let occ_step_eq s1 s2 = match s1, s2 with | O_left, O_left | O_right, O_right | O_mono, O_mono -> true | _ -> false -(* chemin identifiant une proposition sous forme du nom de l'hypothèse et - d'une liste de pas à partir de la racine de l'hypothèse *) +(* chemin identifiant une proposition sous forme du nom de l'hypothèse et + d'une liste de pas à partir de la racine de l'hypothèse *) type occurence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) @@ -63,7 +63,7 @@ type oformula = (* Operators for comparison recognized by Omega *) type comparaison = Eq | Leq | Geq | Gt | Lt | Neq -(* Type des prédicats réifiés (fragment de calcul propositionnel. Les +(* Type des prédicats réifiés (fragment de calcul propositionnel. Les * quantifications sont externes au langage) *) type oproposition = Pequa of Term.constr * oequation @@ -75,19 +75,19 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou proposiitions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) e_left: oformula; (* formule brute gauche *) e_right: oformula; (* formule brute droite *) e_trace: Term.constr; (* tactique de normalisation *) - e_origin: occurence; (* l'hypothèse dont vient le terme *) - e_negated: bool; (* vrai si apparait en position nié - après normalisation *) + e_origin: occurence; (* l'hypothèse dont vient le terme *) + e_negated: bool; (* vrai si apparait en position nié + après normalisation *) e_depends: direction list; (* liste des points de disjonction dont - dépend l'accès à l'équation avec la - direction (branche) pour y accéder *) - e_omega: afine (* la fonction normalisée *) + dépend l'accès à l'équation avec la + direction (branche) pour y accéder *) + e_omega: afine (* la fonction normalisée *) } (* \subsection{Proof context} @@ -106,8 +106,8 @@ type environment = { mutable props : Term.constr list; (* Les variables introduites par omega *) mutable om_vars : (oformula * int) list; - (* Traduction des indices utilisés ici en les indices finaux utilisés par - * la tactique Omega après dénombrement des variables utiles *) + (* Traduction des indices utilisés ici en les indices finaux utilisés par + * la tactique Omega après dénombrement des variables utiles *) real_indices : (int,int) Hashtbl.t; mutable cnt_connectors : int; equations : (int,oequation) Hashtbl.t; @@ -115,35 +115,35 @@ type environment = { } (* \subsection{Solution tree} - Définition d'une solution trouvée par Omega sous la forme d'un identifiant, - d'un ensemble d'équation dont dépend la solution et d'une trace *) -(* La liste des dépendances est triée et sans redondance *) + Définition d'une solution trouvée par Omega sous la forme d'un identifiant, + d'un ensemble d'équation dont dépend la solution et d'une trace *) +(* La liste des dépendances est triée et sans redondance *) type solution = { s_index : int; s_equa_deps : int list; s_trace : action list } -(* Arbre de solution résolvant complètement un ensemble de systèmes *) +(* Arbre de solution résolvant complètement un ensemble de systèmes *) type solution_tree = Leaf of solution - (* un noeud interne représente un point de branchement correspondant à - l'élimination d'un connecteur générant plusieurs buts + (* un noeud interne représente un point de branchement correspondant à + l'élimination d'un connecteur générant plusieurs buts (typ. disjonction). Le premier argument est l'identifiant du connecteur *) | Tree of int * solution_tree * solution_tree -(* Représentation de l'environnement extrait du but initial sous forme de - chemins pour extraire des equations ou d'hypothèses *) +(* Représentation de l'environnement extrait du but initial sous forme de + chemins pour extraire des equations ou d'hypothèses *) type context_content = CCHyp of occurence | CCEqua of int (* \section{Specific utility functions to handle base types} *) -(* Nom arbitraire de l'hypothèse codant la négation du but final *) +(* Nom arbitraire de l'hypothèse codant la négation du but final *) let id_concl = Names.Id.of_string "__goal__" -(* Initialisation de l'environnement de réification de la tactique *) +(* Initialisation de l'environnement de réification de la tactique *) let new_environment () = { terms = []; props = []; om_vars = []; cnt_connectors = 0; real_indices = Hashtbl.create 7; @@ -151,17 +151,17 @@ let new_environment () = { constructors = Hashtbl.create 7; } -(* Génération d'un nom d'équation *) +(* Génération d'un nom d'équation *) let new_connector_id env = env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors -(* Calcul de la branche complémentaire *) +(* Calcul de la branche complémentaire *) let barre = function Left x -> Right x | Right x -> Left x -(* Identifiant associé à une branche *) +(* Identifiant associé à une branche *) let indice = function Left x | Right x -> x -(* Affichage de l'environnement de réification (termes et propositions) *) +(* Affichage de l'environnement de réification (termes et propositions) *) let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" @@ -189,12 +189,12 @@ let new_omega_var, rst_omega_var = (function () -> incr cpt; !cpt), (function () -> cpt:=0) -(* Affichage des variables d'un système *) +(* Affichage des variables d'un système *) let display_omega_var i = Printf.sprintf "OV%d" i -(* Recherche la variable codant un terme pour Omega et crée la variable dans - l'environnement si il n'existe pas. Cas ou la variable dans Omega représente +(* Recherche la variable codant un terme pour Omega et crée la variable dans + l'environnement si il n'existe pas. Cas ou la variable dans Omega représente le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = @@ -204,22 +204,22 @@ let intern_omega env t = env.om_vars <- (t,v) :: env.om_vars; v end -(* Ajout forcé d'un lien entre un terme et une variable Cas où la - variable est créée par Omega et où il faut la lier après coup à un atome - réifié introduit de force *) +(* Ajout forcé d'un lien entre un terme et une variable Cas où la + variable est créée par Omega et où il faut la lier après coup à un atome + réifié introduit de force *) let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars -(* Récupère le terme associé à une variable *) +(* Récupère le terme associé à une variable *) let unintern_omega env id = let rec loop = function [] -> failwith "unintern" | ((t,j)::l) -> if Int.equal id j then t else loop l in loop env.om_vars -(* \subsection{Gestion des environnements de variable pour la réflexion} +(* \subsection{Gestion des environnements de variable pour la réflexion} Gestion des environnements de traduction entre termes des constructions - non réifiés et variables des termes reifies. Attention il s'agit de - l'environnement initial contenant tout. Il faudra le réduire après + non réifiés et variables des termes reifies. Attention il s'agit de + l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) let add_reified_atom t env = @@ -238,24 +238,24 @@ let add_prop env t = with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i -(* accès a une proposition *) +(* accès a une proposition *) let get_prop v env = try List.nth v env with Invalid_argument _ -> failwith "get_prop" -(* \subsection{Gestion du nommage des équations} *) +(* \subsection{Gestion du nommage des équations} *) (* Ajout d'une equation dans l'environnement de reification *) let add_equation env e = let id = e.e_omega.id in try let _ = Hashtbl.find env.equations id in () with Not_found -> Hashtbl.add env.equations id e -(* accès a une equation *) +(* accès a une equation *) let get_equation env id = try Hashtbl.find env.equations id with Not_found as e -> - Printf.printf "Omega Equation %d non trouvée\n" id; raise e + Printf.printf "Omega Equation %d non trouvée\n" id; raise e -(* Affichage des termes réifiés *) +(* Affichage des termes réifiés *) let rec oprint ch = function | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 @@ -289,7 +289,7 @@ let rec weight env = function | Oufo _ -> -1 | Oatom _ as c -> (intern_omega env c) -(* \section{Passage entre oformules et représentation interne de Omega} *) +(* \section{Passage entre oformules et représentation interne de Omega} *) (* \subsection{Oformula vers Omega} *) @@ -332,12 +332,12 @@ let coq_of_formula env t = | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in loop t -(* \subsection{Oformula vers COQ reifié} *) +(* \subsection{Oformula vers COQ reifié} *) let reified_of_atom env i = try Hashtbl.find env.real_indices i with Not_found -> - Printf.printf "Atome %d non trouvé\n" i; + Printf.printf "Atome %d non trouvé\n" i; Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; raise Not_found @@ -390,7 +390,7 @@ let reified_of_proposition env f = try reified_of_proposition env f with reraise -> pprint stderr f; raise reraise -(* \subsection{Omega vers COQ réifié} *) +(* \subsection{Omega vers COQ réifié} *) let reified_of_omega env body constant = let coeff_constant = @@ -407,13 +407,13 @@ let reified_of_omega env body c = try reified_of_omega env body c with reraise -> display_eq display_omega_var (body,c); raise reraise -(* \section{Opérations sur les équations} -Ces fonctions préparent les traces utilisées par la tactique réfléchie -pour faire des opérations de normalisation sur les équations. *) +(* \section{Opérations sur les équations} +Ces fonctions préparent les traces utilisées par la tactique réfléchie +pour faire des opérations de normalisation sur les équations. *) -(* \subsection{Extractions des variables d'une équation} *) -(* Extraction des variables d'une équation. *) -(* Chaque fonction retourne une liste triée sans redondance *) +(* \subsection{Extractions des variables d'une équation} *) +(* Extraction des variables d'une équation. *) +(* Chaque fonction retourne une liste triée sans redondance *) let (@@) = List.merge_uniq compare @@ -482,7 +482,7 @@ let rec negate = function let norm l = (List.length l) -(* \subsection{Mélange (fusion) de deux équations} *) +(* \subsection{Mélange (fusion) de deux équations} *) (* \subsubsection{Version avec coefficients} *) let shuffle_path k1 e1 k2 e2 = let rec loop = function @@ -531,7 +531,7 @@ let rec shuffle env (t1,t2) = do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) else do_list [],Oplus(t1,t2) -(* \subsection{Fusion avec réduction} *) +(* \subsection{Fusion avec réduction} *) let shrink_pair f1 f2 = begin match f1,f2 with @@ -563,7 +563,7 @@ let reduce_factor = function [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) | t -> Errors.error "reduce_factor.1" -(* \subsection{Réordonnancement} *) +(* \subsection{Réordonnancement} *) let rec condense env = function Oplus(f1,(Oplus(f2,r) as t)) -> @@ -596,7 +596,7 @@ let rec condense env = function let final = Oplus(t',Oint zero) in tac @ [Lazy.force coq_c_red6], final -(* \subsection{Elimination des zéros} *) +(* \subsection{Elimination des zéros} *) let rec clear_zero = function Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero -> @@ -607,7 +607,7 @@ let rec clear_zero = function (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t) | t -> [],t;; -(* \subsection{Transformation des hypothèses} *) +(* \subsection{Transformation des hypothèses} *) let rec reduce env = function Oplus(t1,t2) -> @@ -642,7 +642,7 @@ let normalize_linear_term env t = let trace3,t3 = clear_zero t2 in do_list [trace1; do_list trace2; do_list trace3], t3 -(* Cette fonction reproduit très exactement le comportement de [p_invert] *) +(* Cette fonction reproduit très exactement le comportement de [p_invert] *) let negate_oper = function Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq @@ -668,7 +668,7 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = INEQ with e when Logic.catchable_exception e -> raise e -(* \section{Compilation des hypothèses} *) +(* \section{Compilation des hypothèses} *) let rec oformula_of_constr env t = match Z.parse_term t with @@ -697,7 +697,7 @@ and binprop env (neg2,depends,origin,path) oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in - (* On numérote le connecteur dans l'environnement. *) + (* On numérote le connecteur dans l'environnement. *) c i t1' t2' and mk_equation env ctxt c connector t1 t2 = @@ -736,7 +736,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c -(* Destructuration des hypothèses et de la conclusion *) +(* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = let concl = Tacmach.pf_concl gl in @@ -819,9 +819,9 @@ let destructurate_hyps syst = | [] -> [[]] in loop syst -(* \subsection{Affichage d'un système d'équation} *) +(* \subsection{Affichage d'un système d'équation} *) -(* Affichage des dépendances de système *) +(* Affichage des dépendances de système *) let display_depend = function Left i -> Printf.printf " L%d" i | Right i -> Printf.printf " R%d" i @@ -852,8 +852,8 @@ let display_systems syst_list = List.iter display_equation syst in List.iter display_system syst_list -(* Extraction des prédicats utilisées dans une trace. Permet ensuite le - calcul des hypothèses *) +(* Extraction des prédicats utilisées dans une trace. Permet ensuite le + calcul des hypothèses *) let rec hyps_used_in_trace = function | act :: l -> @@ -865,9 +865,9 @@ let rec hyps_used_in_trace = function end | [] -> [] -(* Extraction des variables déclarées dans une équation. Permet ensuite - de les déclarer dans l'environnement de la procédure réflexive et - éviter les créations de variable au vol *) +(* Extraction des variables déclarées dans une équation. Permet ensuite + de les déclarer dans l'environnement de la procédure réflexive et + éviter les créations de variable au vol *) let rec variable_stated_in_trace = function | act :: l -> @@ -885,7 +885,7 @@ let rec variable_stated_in_trace = function let add_stated_equations env tree = (* Il faut trier les variables par ordre d'introduction pour ne pas risquer - de définir dans le mauvais ordre *) + de définir dans le mauvais ordre *) let stated_equations = let cmpvar x y = Pervasives.(-) x.st_var y.st_var in let rec loop = function @@ -894,15 +894,15 @@ let add_stated_equations env tree = in loop tree in let add_env st = - (* On retransforme la définition de v en formule reifiée *) + (* On retransforme la définition de v en formule reifiée *) let v_def = oformula_of_omega env st.st_def in - (* Notez que si l'ordre de création des variables n'est pas respecté, + (* Notez que si l'ordre de création des variables n'est pas respecté, * ca va planter *) let coq_v = coq_of_formula env v_def in let v = add_reified_atom coq_v env in (* Le terme qu'il va falloir introduire *) let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in - (* sa représentation sous forme d'équation mais non réifié car on n'a pas + (* sa représentation sous forme d'équation mais non réifié car on n'a pas * l'environnement pour le faire correctement *) let term_to_reify = (v_def,Oatom v) in (* enregistre le lien entre la variable omega et la variable Coq *) @@ -910,8 +910,8 @@ let add_stated_equations env tree = (v, term_to_generalize,term_to_reify,st.st_def.id) in List.map add_env stated_equations -(* Calcule la liste des éclatements à réaliser sur les hypothèses - nécessaires pour extraire une liste d'équations donnée *) +(* Calcule la liste des éclatements à réaliser sur les hypothèses + nécessaires pour extraire une liste d'équations donnée *) (* PL: experimentally, the result order of the following function seems _very_ crucial for efficiency. No idea why. Do not remove the List.rev @@ -958,7 +958,7 @@ let really_useful_prop l_equa c = | Pnot t1 -> app coq_not [|real_of t1|] | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|] | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|] - (* Attention : implications sur le lifting des variables à comprendre ! *) + (* Attention : implications sur le lifting des variables à comprendre ! *) | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2) | Pprop t -> t in let rec loop c = @@ -1166,11 +1166,11 @@ and decompose_tree_hyps trace env ctxt = function (* \section{La fonction principale} *) (* Cette fonction construit la -trace pour la procédure de décision réflexive. A partir des résultats -de l'extraction des systèmes, elle lance la résolution par Omega, puis +trace pour la procédure de décision réflexive. A partir des résultats +de l'extraction des systèmes, elle lance la résolution par Omega, puis l'extraction d'un ensemble minimal de solutions permettant la -résolution globale du système et enfin construit la trace qui permet -de faire rejouer cette solution par la tactique réflexive. *) +résolution globale du système et enfin construit la trace qui permet +de faire rejouer cette solution par la tactique réflexive. *) let resolution env full_reified_goal systems_list = let num = ref 0 in @@ -1181,7 +1181,7 @@ let resolution env full_reified_goal systems_list = simplify_strong (new_omega_eq,new_omega_var,display_omega_var) system in - (* calcule les hypotheses utilisées pour la solution *) + (* calcule les hypotheses utilisées pour la solution *) let vars = hyps_used_in_trace trace in let splits = get_eclatement env vars in if !debug then begin @@ -1202,7 +1202,7 @@ let resolution env full_reified_goal systems_list = display_solution_tree stdout solution_tree; print_newline() end; - (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) + (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) let useful_equa_id = equas_of_solution_tree solution_tree in (* recupere explicitement ces equations *) let equations = List.map (get_equation env) useful_equa_id in @@ -1225,8 +1225,8 @@ let resolution env full_reified_goal systems_list = let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in (* L'environnement de base se construit en deux morceaux : - - les variables des équations utiles (et de la conclusion) - - les nouvelles variables declarées durant les preuves *) + - les variables des équations utiles (et de la conclusion) + - les nouvelles variables declarées durant les preuves *) let all_vars_env = useful_vars @ stated_vars in let basic_env = let rec loop i = function @@ -1236,7 +1236,7 @@ let resolution env full_reified_goal systems_list = | [] -> [] in loop 0 all_vars_env in let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in - (* On peut maintenant généraliser le but : env est a jour *) + (* On peut maintenant généraliser le but : env est a jour *) let l_reified_stated = List.map (fun (_,_,(l,r),_) -> app coq_p_eq [| reified_of_formula env l; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 0e7804bc7..740175688 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -232,7 +232,7 @@ let rec norm_head info env t stack = let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack else - (CBN(t,env), stack) (* Considérer une coupure commutative ? *) + (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> (match evar_value info.i_cache ev with diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ae1c4eea0..54621eb9d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -399,7 +399,7 @@ type coercion = { coercion_params : int; } -(* Calcul de l'arité d'une classe *) +(* Computation of the class arity *) let reference_arity_length ref = let t = Universes.unsafe_type_of_global ref in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 504d73cb8..ae9210e49 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -9,7 +9,7 @@ (* Created by Hugo Herbelin for Coq V7 by isolating the coercion mechanism out of the type inference algorithm in file trad.ml from Coq V6.3, Nov 1999; The coercion mechanism was implemented in - trad.ml by Amokrane Saïbi, May 1996 *) + trad.ml by Amokrane Saïbi, May 1996 *) (* Addition of products and sorts in canonical structures by Pierre Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) @@ -345,7 +345,7 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd -(* appliquer le chemin de coercions p à hj *) +(* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7a1f155bd..27c1e1e7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -180,11 +180,11 @@ let computable p k = A solution could be to store, in the MutCase, the eta-expanded normal form of pred to decide if it depends on its variables - Lorsque le prédicat est dépendant de manière certaine, on - ne déclare pas le prédicat synthétisable (même si la - variable dépendante ne l'est pas effectivement) parce que - sinon on perd la réciprocité de la synthèse (qui, lui, - engendrera un prédicat non dépendant) *) + Lorsque le prédicat est dépendant de manière certaine, on + ne déclare pas le prédicat synthétisable (même si la + variable dépendante ne l'est pas effectivement) parce que + sinon on perd la réciprocité de la synthèse (qui, lui, + engendrera un prédicat non dépendant) *) let sign,ccl = decompose_lam_assum p in Int.equal (rel_context_length sign) (k + 1) @@ -644,7 +644,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran | _, false::l -> (* eta-expansion : n'arrivera plus lorsque tous les - termes seront construits à partir de la syntaxe Cases *) + termes seront construits à partir de la syntaxe Cases *) (* nommage de la nouvelle variable *) let new_b = applist (lift 1 b, [mkRel 1]) in let pat,new_avoid,new_env,new_ids = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index cce0ff5ec..661aa8b7a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -73,8 +73,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = in let ndepar = mip.mind_nrealdecls + 1 in - (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) - (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) + (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) + (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) let env' = push_rel_context lnamespar env in @@ -241,7 +241,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = in prec env 0 [] in - (* ici, cstrprods est la liste des produits du constructeur instantié *) + (* ici, cstrprods est la liste des produits du constructeur instantié *) let rec process_constr env i f = function | (n,None,t as d)::cprest, recarg::rest -> let optionpos = diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index a6c0149a4..ed4bc4d39 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -176,8 +176,8 @@ let next_ident_away_from id bad = let restart_subscript id = if not (has_subscript id) then id else - (* Ce serait sans doute mieux avec quelque chose inspiré de - *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) + (* It would probably be better with something in the spirit of + *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id let rec to_avoid id = function diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 0576ec57b..afb1c9475 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -325,7 +325,7 @@ let rec pat_of_raw metas vars = function metas := n::!metas; PMeta (Some n) | GRef (_,gr,_) -> PRef (canonical_gr gr) - (* Hack pour ne pas réécrire une interprétation complète des patterns*) + (* Hack to avoid rewriting a complete interpretation of patterns *) | GApp (_, GPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (_,c,cl) -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 66aa85ecd..f836c2327 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Created by Amokrane Saïbi, Dec 1998 *) +(* Created by Amokrane Saïbi, Dec 1998 *) (* Addition of products and sorts in canonical structures by Pierre Corbineau, Feb 2008 *) @@ -28,10 +28,10 @@ open Reductionops constructor (the name of which defaults to Build_S) *) (* Table des structures: le nom de la structure (un [inductive]) donne - le nom du constructeur, le nombre de paramètres et pour chaque - argument réel du constructeur, le nom de la projection - correspondante, si valide, et un booléen disant si c'est une vraie - projection ou bien une fonction constante (associée à un LetIn) *) + le nom du constructeur, le nombre de paramètres et pour chaque + argument réel du constructeur, le nom de la projection + correspondante, si valide, et un booléen disant si c'est une vraie + projection ou bien une fonction constante (associée à un LetIn) *) type struc_typ = { s_CONST : constructor; diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 75c8fb424..72f87a19e 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -851,9 +851,9 @@ let align_prod_letin c a : rel_context * constr = let (l1,l2) = Util.List.chop lc l in l2,it_mkProd_or_LetIn a l1 -(* On reduit une serie d'eta-redex de tete ou rien du tout *) +(* We reduce a series of head eta-redex or nothing at all *) (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) -(* Remplace 2 versions précédentes buggées *) +(* Remplace 2 earlier buggish versions *) let rec eta_reduce_head c = match kind_of_term c with diff --git a/tactics/elim.ml b/tactics/elim.ml index ba413d410..c83441894 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -77,10 +77,10 @@ and general_decompose_aux recognizer id = (ids_of_named_context bas.Tacticals.assums)))) id -(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste - pas si aucune élimination n'est possible *) +(* We should add a COMPLETE to be sure that the created hypothesis + doesn't stay if no elimination is possible *) -(* Meilleures stratégies mais perte de compatibilité *) +(* Best strategies but loss of compatibility *) let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7eb81c3f4..d0946e2ad 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -242,7 +242,7 @@ let add_inversion_lemma_exn na com comsort bool tac = try add_inversion_lemma na env sigma c sort bool tac with - | UserError ("Case analysis",s) -> (* référence à Indrec *) + | UserError ("Case analysis",s) -> (* Reference to Indrec *) errorlabstrm "Inv needs Nodep Prop Set" s (* ================================= *) diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el index 05618a041..068e64002 100644 --- a/tools/coq-font-lock.el +++ b/tools/coq-font-lock.el @@ -110,18 +110,18 @@ syntax colouring behaviour.") ;;A new face for tactics (defface coq-solve-tactics-face (proof-face-specs - (:foreground "forestgreen" t) ; pour les fonds clairs - (:foreground "forestgreen" t) ; pour les fond foncés - ()) ; pour le noir et blanc + (:foreground "forestgreen" t) ; for bright backgrounds + (:foreground "forestgreen" t) ; for dark backgrounds + ()) ; for black and white "Face for names of closing tactics in proof scripts." :group 'proof-faces) ;;A new face for tactics which fail when they don't kill the current goal (defface coq-solve-tactics-face (proof-face-specs - (:foreground "red" t) ; pour les fonds clairs - (:foreground "red" t) ; pour les fond foncés - ()) ; pour le noir et blanc + (:foreground "red" t) ; for bright backgrounds + (:foreground "red" t) ; for dark backgrounds + ()) ; for black and white "Face for names of closing tactics in proof scripts." :group 'proof-faces) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 587b5c064..e4656d240 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* créer un Makefile pour un développement Coq automatiquement *) +(* Coq_makefile: automatically create a Makefile for a Coq development *) let output_channel = ref stdout let makefile_name = ref "Makefile" diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 9de9a38ff..f49f9f006 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -1,5 +1,5 @@ -% This is coqdoc.sty, by Jean-Christophe Filliâtre +% This is coqdoc.sty, by Jean-Christophe Filliâtre % This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc) % % You can modify the following macros to customize the appearance diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 88a102d85..f67ab5f95 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -450,7 +450,7 @@ let gen_mult_files l = if (!header_trailer) then Output.trailer (); close_out_file() end - (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) + (* NB: for latex and texmacs, a separated toc or index is meaningless... *) let read_glob_file vfile f = try Index.read_glob vfile f diff --git a/tools/gallina.el b/tools/gallina.el index 7af2d765f..cbc13118a 100644 --- a/tools/gallina.el +++ b/tools/gallina.el @@ -1,7 +1,7 @@ ;; gallina.el --- Coq mode editing commands for Emacs ;; ;; Jean-Christophe Filliatre, march 1995 -;; Honteusement pompé de caml.el, Xavier Leroy, july 1993. +;; Shamelessly copied from caml.el, Xavier Leroy, july 1993. ;; ;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior diff --git a/toplevel/class.ml b/toplevel/class.ml index 6e95a930d..e1d4140e5 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -178,7 +178,7 @@ let ident_key_of_class = function | CL_IND (sp,_) -> Label.to_string (mind_label sp) | CL_SECVAR id -> Id.to_string id -(* coercion identité *) +(* Identity coercion *) let error_not_transparent source = errorlabstrm "build_id_coercion" |