aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2005-03-15Unsharing before exportation to ensure uniqueness of xml id'sherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à ↵herbelin
l'inefficacité montrée dans le bug #932: suppression plutôt des Anonymous dans le contexte des evars (cf Evarutil) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6836 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6834 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6832 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6830 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-12Explicitation d'un nom de variable nécessaire au bon typage, suite à ↵herbelin
suppression des _ du contexte des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6829 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-12Backtrack version 1.82 awaiting for better understanding of the consequences ↵herbelin
of removing Anonymous from evars contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6828 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6826 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-11Méthode plus raisonnable pour supprimer l'inefficacité des evars ↵herbelin
dépendantes de Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6825 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:21:35 +0000