coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
\| \| \| \| \| \| \| \|	"Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
*	improve the amount of information given by the Ltac tactic debugger	bertot	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin	2006-02-07
\| \| \| \| \| \| \|	prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ↵	herbelin	2006-01-21
\| \| \| \| \| \|	et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7911 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵	herbelin	2005-12-17
\| \| \| \| \| \|	(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵	herbelin	2005-12-17
\| \| \| \| \| \|	et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 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
*	Adaptation a la v7 du message d'erreur Match_failure	herbelin	2004-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	search window	coq	2004-02-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage Assert_failure en ocaml 3.07	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un message à FailTac	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debugger plus informatif	delahaye	2003-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	msg Failtac; echec -batch s'il reste des preuves	filliatr	2003-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3525 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
*	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@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug d'affichage des erreurs localisées dans un fichier suite à	herbelin	2002-03-27
\| \| \| \| \| \| \|	changement de précédence de ++, anciennement [< ; >], vis à vis du if git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2572 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