aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-05-02Utilisation Z_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6980 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6978 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6976 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug ↵herbelin
#901) (continued!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6975 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug ↵herbelin
#901) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6974 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29Improved order of interpretation of atomic tactics (cf bug #952)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6972 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-29Fix bug in prepare_predicate_from_tycon; improved error message when no ↵herbelin
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
2005-04-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6967 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6965 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6963 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6960 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6958 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6956 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6954 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6952 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6951 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6950 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6948 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
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
2005-04-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6945 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6943 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6941 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6939 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6937 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6935 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6933 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6931 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6929 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6927 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6925 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6923 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6921 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6920 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-07dp: traitement des definitionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6919 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6917 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6915 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-05Problemes de renommage reglescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6914 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6912 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6910 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6908 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6906 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6904 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-31Added option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6901 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6899 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵herbelin
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
2005-03-29Missing translating a 'O' into a '0' (again)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6894 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:54:50 +0000