coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	maj	filliatr	2002-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction vers scheme	letouzey	2002-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affaiblissement hyp de Zmult_reg_left	filliatr	2002-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	jLogic disparaît	herbelin	2002-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2649 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backtrack dans l'algo d'unification	barras	2002-04-10
\| \| \| \| \| \| \|	fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An intuitionistic first-order theorem prover -- JProver.	huang	2002-03-22
\| \| \| \| \| \| \|	See the "README" file for more information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile	courant	2002-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Big commit extraction:	letouzey	2002-03-04
\| \| \| \| \| \| \| \| \| \| \|	- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce	ddr	2002-02-20
\| \| \| \| \| \| \| \|	qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
\| \| \| \| \| \| \|	- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	substitution et pattern modulo let	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement generation de schema d'elimination, False_rec est primitif, ↵	mohring	2002-01-31
\| \| \| \| \| \|	Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2002-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	contrib/interface/dad.ml4 had no real need of streams, it should have been	bertot	2001-12-19
\| \| \| \| \| \| \| \|	translated into a regular ml files like the others. This mistake is now corrected. The Makefile and dependency files are updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2345 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du make depend et du .depend	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2333 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation de make doc (ocamlweb & _)	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add dependencies for two new files in contrib/interface	bertot	2001-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2314 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise a jour des dependances	clrenard	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2249 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour	filliatr	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour	filliatr	2001-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un fichier Max dans Arith, et enrichissement du Min.	letouzey	2001-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-11-05
\| \| \| \| \| \| \| \| \| \|	- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵	letouzey	2001-10-26
\| \| \| \| \| \|	ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵	letouzey	2001-10-22
\| \| \| \| \| \|	options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de dynamiques pour les quotations constr et tactic	delahaye	2001-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparent	barras	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement des setoides.	clrenard	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de l'emplacement des fichiers pour les setoides.	clrenard	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Romega/names/Makefile	mohring	2001-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing	herbelin	2001-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVE	herbelin	2001-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Module : CONSTR/V7 Working dir: ~/V7uo/ In directory .: Modified .depend Modified CHANGES Unknown COMMIT Modified Makefile Modified TODO Unknown log.up Unknown parsing-sans-slam Unknown titi.v Unknown toto.v In directory contrib: Unknown contrib/interface_essai Unknown contrib/log In directory contrib/correctness: Modified contrib/correctness/pcic.ml Modified contrib/correctness/pmisc.ml Modified contrib/correctness/psyntax.ml4 In directory contrib/extraction: Modified contrib/extraction/extract_env.ml Modified contrib/extraction/haskell.ml Modified contrib/extraction/ocaml.ml Modified contrib/extraction/ocaml.mli In directory contrib/field: Modified contrib/field/field.ml4 Message: cvs server: New directory `contrib/interface' -- ignored Unknown contrib/interface/ctast.ml In directory contrib/omega: Modified contrib/omega/coq_omega.ml In directory contrib/ring: Modified contrib/ring/Setoid_ring_normalize.v Modified contrib/ring/quote.ml Modified contrib/ring/ring.ml Message: cvs server: New directory `contrib/setoid' -- ignored In directory contrib/xml: Modified contrib/xml/xmlcommand.ml In directory dev: Modified dev/base_include Modified dev/top_printers.ml In directory kernel: Modified kernel/cooking.ml Modified kernel/cooking.mli Modified kernel/environ.ml Modified kernel/environ.mli Unknown kernel/identifier.ml Unknown kernel/identifier.mli Modified kernel/names.ml Modified kernel/names.mli Modified kernel/safe_typing.mli Modified kernel/univ.ml In directory lib: Modified lib/system.ml Modified lib/system.mli Modified lib/util.ml Modified lib/util.mli In directory library: Modified library/declare.ml Modified library/declare.mli Modified library/global.ml Modified library/global.mli Modified library/lib.ml Modified library/lib.mli Modified library/library.ml Modified library/library.mli Modified library/nametab.ml Unknown library/nametab.ml.copie Unknown library/nametab.ml.saved Modified library/nametab.mli Unknown library/nametab.mli.saved In directory parsing: Modified parsing/ast.ml Modified parsing/ast.mli Modified parsing/astterm.ml Modified parsing/coqast.ml Modified parsing/coqast.mli Modified parsing/coqlib.ml Modified parsing/coqlib.mli Modified parsing/esyntax.ml Modified parsing/extend.ml4 Modified parsing/g_basevernac.ml4 Modified parsing/g_cases.ml4 Modified parsing/g_constr.ml4 Modified parsing/g_ltac.ml4 Modified parsing/g_prim.ml4 Modified parsing/g_rsyntax.ml Modified parsing/g_tactic.ml4 Modified parsing/g_vernac.ml4 Modified parsing/g_zsyntax.ml Modified parsing/lexer.ml4 Modified parsing/pcoq.ml4 Modified parsing/pcoq.mli Modified parsing/pretty.ml Modified parsing/prettyp.ml Modified parsing/printer.ml Modified parsing/q_coqast.ml4 Modified parsing/search.ml Modified parsing/termast.ml In directory pretyping: Modified pretyping/classops.ml Modified pretyping/syntax_def.ml In directory proofs: Modified proofs/proof_trees.ml Modified proofs/tacinterp.ml Modified proofs/tacinterp.mli In directory tactics: Modified tactics/Inv.v Modified tactics/dhyp.ml Modified tactics/inv.ml Modified tactics/inv.mli Modified tactics/setoid_replace.ml Modified tactics/tacticals.ml Modified tactics/tactics.ml Modified tactics/tauto.ml4 In directory test-suite: Unknown test-suite/vernac In directory theories: Message: cvs server: New directory `theories/Zarith' -- ignored In directory toplevel: Modified toplevel/class.ml Modified toplevel/command.ml Modified toplevel/command.mli Modified toplevel/coqinit.ml Modified toplevel/coqtop.ml Modified toplevel/discharge.ml Modified toplevel/discharge.mli Modified toplevel/mltop.ml4 Modified toplevel/record.ml Modified toplevel/vernacentries.ml Modified toplevel/vernacinterp.ml --------------------- End --------------------- -- last cmd: cvs -f -n update -d -P -- git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de place et de nom de la tactique Setoid_rewrite.	clrenard	2001-07-10
\| \| \| \| \| \| \|	Maintenant On appelle Rewrite et il choisit si c'est un setoide ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1838 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise a jour des .depend	clrenard	2001-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1809 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵	herbelin	2001-06-25
\| \| \| \| \| \|	définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵	herbelin	2001-06-25
\| \| \| \| \| \|	compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension des parametres de Clear	delahaye	2001-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des entrees puor Setoid_replace.	clrenard	2001-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pretty -> Prettyp	filliatr	2001-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise en place extraction haskell	filliatr	2001-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Rseries et Rtrigo_fun	mayero	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Fourier, DiscrR, ...	mayero	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1656 85f007b7-540e-0410-9357-904b9bb8a0f7