coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	maj	coq	2005-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	possibilité d'écrire [foo\| ] au lieu de [foo\|idtac]	letouzey	2005-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	possibilité d'écrire [foo\| ] au lieu de [foo\|idtac]	letouzey	2005-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage graphe univers	herbelin	2005-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6994 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code v7 obsolete	herbelin	2005-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ commentaires et inversion du sens du graphe de contraintes pour ↵	herbelin	2005-05-05
\| \| \| \| \| \|	extensibilité aux contraintes numériques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6990 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Open Scope non Local malencontreux	herbelin	2005-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6985 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵	herbelin	2005-05-02
\| \| \| \| \| \|	plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Lemme de passage de l'autre côté d'une égalité	herbelin	2005-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation Z_scope	herbelin	2005-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-05-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6978 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6976 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) (continued!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved order of interpretation of atomic tactics (cf bug #952)	herbelin	2005-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug in prepare_predicate_from_tycon; improved error message when no ↵	herbelin	2005-04-29
\| \| \| \| \| \|	clauses and no empty inductive type found; (expected) improvement in the shifting test (match_current) on non inductive type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6969 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6967 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed hypotheses of Z_lt_induction (see #957)	herbelin	2005-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6960 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6958 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6954 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-04-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6952 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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