coq - The formal proof system

Age	Commit message (Collapse)	Author
2002-12-03	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot
	syntaxes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3362 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-06	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot
	and associated file. Also adding a systematic check approach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3092 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-03	Previous version did compile but did not make it possible to actually run	bertot
	pcoq. This version does work. Main modification is: - change centaur.ml4 so that * the Pcoq mode is really started by Start Pcoq Mode. * Reset <id> and Reset Initial work as planned for Pcoq (commands are Pcoq Reset <id> and Pcoq ResetInitial). * current_proof_name() does not raise an exception when there is no current proof. - change xlate.ml so that the main tacticals are translated correctly to pcoq data structures. - change in ascent.mli so that * we make sure Fail can now have a numeric argument, * progress is added - vtp.ml is changed in accordance with ascent.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3078 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18	Integrating the Ltac language and the Blast tool into the interface	bertot
	capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05	GROS COMMIT:	barras
	- 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
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-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