coq - The formal proof system

Age	Commit message (Collapse)	Author
2001-05-29	Facilites pour le debogguage des univers.	coq
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28	Pretty -> Prettyp	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03	Changement de la structure des points fixes	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24	Removing a debug message for the search command.	bertot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1678 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19	Add a treatement of elaborate Intros tactics, CONJPATTERN and family.	bertot
	This may not be complete, but it already handles simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1638 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19	ZArith --> Zarith	mohring
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1627 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19	remplace Zarith par ZArith	mohring
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19	Making sure there will be no warnings at compile time.	bertot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1614 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18	Correcting a problem of s that appears behind a Let when there are	bertot
	several variables introduced (showproof.ml) Added CASTEDOPENCOMMAND, QUALIDCONSTARG as variants in several places (xlate.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1604 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18	Changing the commands to switch to textual explanation of proofs.	bertot
	Removing the "Show Dad Rules." command that breaks down parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1600 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18	Adding files for the production of textual explanations as used in pcoq.	bertot
	dependence files are updated accordingly. Modifications in other files to cope with a few errors in the translation for the parser (mostly around records, coercions, and the search-pattern command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-07	Make sure the parser knows about the constructors of type nat, so	bertot
	that specific syntax for this type can be parsed and translated to tree structures. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1555 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-07	Two constants had been given in the wrong package (Logic_type instead of	bertot
	the correct Logic_Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1554 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵	filliatr
	d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04	These files are used to construct an independent parser, that is a small	bertot
	coq that is only able to parse coq script files and produced a tree-like representation. For now this representation is only given in a postfix format, but other format (such as XML) could also be possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1540 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04	These files are loaded coq-interface to make a process that is "pcoq" enabled.	bertot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1539 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04	Make sure the constructors of Z and positive are recognized: they show up	bertot
	when parsing expressions between back-quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1538 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04	Files that handle the dialogue with the graphical user-interface pcoq.	bertot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7