coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	maj	coq	2005-04-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gestion du forall et envoie d'axiome à la procédure	coq	2005-04-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6950 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6948 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	anywhere in a script (provided no suspend/resume is used): * the command "Backtrack n m p" (vernac_bactrack) performs the following operation: do abort p times, do undo on the current proof (after the aborts) in order to reach a stack depth of m (see vernac_undo_todepth) ** resets the global state to state labelled with n. * The coq prompt in emacs mode has more informations, it contains: the usual coq prompt plus: the state number (global state label) the depth of the current proof stack the names of all pending proofs, in unspecified order, separated by '\|' Example: state proof stack num depth __ _ aux < 12 \|aux\|SmallStepAntiReflexive\| 4 < ù ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6943 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6941 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6939 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6937 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6935 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6929 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6923 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	dp: traitement des definitions	coq	2005-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6919 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Problemes de renommage regles	coq	2005-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6914 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6912 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6910 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6906 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6904 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added option_map	herbelin	2005-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6901 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵	herbelin	2005-03-29
\| \| \| \| \| \|	hypothesis of Zlt/Zgt_square_simpl (cg #948) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6898 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing translating a 'O' into a '0' (again)	herbelin	2005-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6890 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6886 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6885 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing translating a 'O' into a '0'	herbelin	2005-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	symboles de fonctions globaux traites	coq	2005-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6879 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de l'axiome du but prouve par la tactique simplifi	coq	2005-03-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Unset Implicit Arguments manquant	herbelin	2005-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug de dependent_hyps qui ne met pas à jour le type des hyps ↵	herbelin	2005-03-20
\| \| \| \| \| \|	dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6868 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵	herbelin	2005-03-20
\| \| \| \| \| \|	hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6865 85f007b7-540e-0410-9357-904b9bb8a0f7