coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add printer for Pp.std_ppcmds...	msozeau	2008-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
\| \| \| \| \| \| \| \| \|	devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
\| \| \| \| \| \| \| \|	Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
\| \| \| \| \| \| \| \| \|	échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rajout du mot Fix dans le printer	vsiles	2007-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retablissement de Fix dans print_pure_constr	vsiles	2007-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allègement de l'affichage des références par le printer si possible	herbelin	2007-01-22
\| \| \| \| \| \| \| \| \| \| \| \|	(on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et pour tous les constructeurs). Pour un affichage complètement explicite des noms avec ocamldebug, charger maintenant set_raw_db en plus de db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export de l'afficheur de substitutions de noms de modules pour le débogueur	herbelin	2007-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tout petit bug d'affichage dans constr_display (top_printers)	herbelin	2006-09-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9161 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plutôt pas de contraction des match dans le déboggueur	herbelin	2006-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout printer Idset.t	herbelin	2006-01-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
\| \| \| \| \| \| \|	et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵	herbelin	2006-01-04
\| \| \| \| \| \|	(suite): correction des dépendances (et notamment non-dépendance en unix.cma) pour la création de printers.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵	herbelin	2006-01-04
\| \| \| \| \| \|	(débranchées depuis mars 01) + affichage plus concis des locations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des ↵	herbelin	2005-12-26
\| \| \| \| \| \|	G_new en G_.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des named_context	gregoire	2005-12-02
\| \| \| \| \| \| \| \|	Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout constant printer	herbelin	2005-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Découpage des printers pour ne pas avoir de dépendances en la vm dans les ↵	herbelin	2005-01-02
\| \| \| \| \| \|	printers de ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6545 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout printer bigint	herbelin	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement dans les boxed values .	gregoire	2004-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	hiding the meta_map in evar_defs	barras	2004-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification encore...	barras	2004-09-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout affichage contexte local	herbelin	2004-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	prettyprint des constr_substituted + un wrapping de prglobal pour qu'il ↵	letouzey	2003-04-16
\| \| \| \| \| \|	n'echoue jamais lors d'un débug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3928 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation tactiques	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Options d'affichage maintenant dans Constrextern	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout affichage fconstr	herbelin	2002-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3382 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'un printer pour les global_reference	letouzey	2002-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
\| \| \| \| \| \| \| \| \| \| \| \| \|	Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petites corrections ici et la	coq	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 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
*	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
*	suppression du retour chariot a la fin de print_pure_constr	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵	herbelin	2001-10-17
\| \| \| \| \| \|	sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 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 du printer de tactiques + modif du Dynamic ocaml	delahaye	2001-09-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 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
*	ajout d'un afficher de contexte et d'une fonction constbody_of_string	letouzey	2001-05-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1739 85f007b7-540e-0410-9357-904b9bb8a0f7