aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2005-03-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6892 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6890 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6888 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6886 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6885 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24Missing translating a 'O' into a '0'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24symboles de fonctions globaux traitescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6882 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6879 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6877 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6876 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6873 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-21Ajout Unset Implicit Arguments manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6870 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-20Correction bug de dependent_hyps qui ne met pas à jour le type des hyps ↵herbelin
dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6868 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-20Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵herbelin
hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6865 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6864 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19Correction erreur grossière de non restauration d'état en cas de retour ↵herbelin
exceptionnel; suppression without_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6863 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19Le type d'un Let est considéré comme 'user-provided' par le noyau et doit ↵herbelin
donc avoir des univers frais git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6862 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19Ajout test bug #935herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6859 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19Report depuis la V8.0pl2 de la correction d'un bug du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6858 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6856 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6855 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-18appel de Simplify depuis Coqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6852 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6851 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6850 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6849 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6848 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6846 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6845 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16MAJ PolyList -> Listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6844 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6843 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6841 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6839 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6838 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 11:22:58 +0000