coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr	2001-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	array_fold_left_i	filliatr	2001-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1550 85f007b7-540e-0410-9357-904b9bb8a0f7
*	axiomes dans les types	filliatr	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de coq_example# dans coq-tex	werner	2001-04-04
\| \| \| \| \| \| \|	BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵	filliatr	2001-04-04
\| \| \| \| \| \|	d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding the dependencies for the parser that is used in the interface pcoq.	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	implification de extract_constr et extract_term	letouzey	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1545 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adding the directives to compile the parser that is used in the graphical	bertot	2001-04-04
\| \| \| \| \| \| \|	interface git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1544 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a flag that makes it possible to re-load files while taking only the	bertot	2001-04-04
\| \| \| \| \| \| \| \| \|	pieces of data for which the system is ready, without raising an exception. This is used to construct a reduced-coq process that can only parse. This reduced-coq is a part of the graphical interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1543 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added two files that are used for the connection with the graphical ↵	bertot	2001-04-04
\| \| \| \| \| \| \| \| \|	user-interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1542 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a flag to avoid sending too many warnings when reloading syntax files	bertot	2001-04-04
\| \| \| \| \| \| \|	in the parser used for the graphical user-interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1541 85f007b7-540e-0410-9357-904b9bb8a0f7
*	These files are used to construct an independent parser, that is a small	bertot	2001-04-04
\| \| \| \| \| \| \| \| \|	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
*	These files are loaded coq-interface to make a process that is "pcoq" enabled.	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make sure the constructors of Z and positive are recognized: they show up	bertot	2001-04-04
\| \| \| \| \| \| \|	when parsing expressions between back-quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a Comments command, that does nothing, but is quite useful to to have	bertot	2001-04-04
\| \| \| \| \| \| \| \|	well displayed comments in the middle of developments (that is comments that are more than just plain strings). Used in the graphical interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1537 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add the binary coq-interface, used for the communication with the graphical	bertot	2001-04-04
\| \| \| \| \| \| \|	user-interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add the compilation of the files needed for the interface with pcoq.	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adding entry points for the arguments of the Comment command.	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding A command for comments, this makes it possible to have structured	bertot	2001-04-04
\| \| \| \| \| \| \|	comments that will be displayed nicely in structured oriented interfaces like pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1533 85f007b7-540e-0410-9357-904b9bb8a0f7
*	dependencies required for contrib/interface	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Files that handle the dialogue with the graphical user-interface pcoq.	bertot	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation	filliatr	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1530 85f007b7-540e-0410-9357-904b9bb8a0f7
*	supression vieux fichiers extraction	filliatr	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1529 85f007b7-540e-0410-9357-904b9bb8a0f7
*	rollback sur les commandes Extract Constant/Inductive; nettoyage et ↵	filliatr	2001-04-04
\| \| \| \| \| \|	documentation code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deux fichiers (past et ptype) uniquement sous forme de .mli	filliatr	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1527 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commandes Extract Constant/Inductive; message d'erreur pour les axiomes	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The function filter_by_module, that was previously exported was not the	bertot	2001-04-03
\| \| \| \| \| \| \|	one that was really needed. I changed it for filter_by_module_from_list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1525 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export a function (build_inductive) that is used in the graphical interface.	bertot	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make sure that the COQTOP variable is really used, when it is set.	bertot	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make it possible to perform proofs by induction even on non-inductive types,	bertot	2001-04-03
\| \| \| \| \| \| \|	as long as one provides the induction principle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ménage	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1521 85f007b7-540e-0410-9357-904b9bb8a0f7
*	psyntax.ml4 sous CVS	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1520 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de Options.if_verbose	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
*	installation des .cmo pour l'extraction	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour pour ocamlweb	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	parenthèses autour des types dans les arguments des constructeurs	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	underscores pour les variables représentant des propositions	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inductifs vides	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ml_pop au lieu de ml_lift dans betared_ast	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1512 85f007b7-540e-0410-9357-904b9bb8a0f7
*	à faire	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1511 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug Fix signalé par Alexandre (even/odd mal interprété)	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1510 85f007b7-540e-0410-9357-904b9bb8a0f7
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de lemmes sur les booleens	mohring	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introduction d'une preuve de False_rec	mohring	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction modulaire	filliatr	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction modulaire + environnement des Fix corrigé	filliatr	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	repertoire pour les tests d'extraction	filliatr	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	application avec bcp args	letouzey	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	beta-reduction	filliatr	2001-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1502 85f007b7-540e-0410-9357-904b9bb8a0f7