aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-07-10Changement de place et de nom de la tactique Setoid_rewrite.clrenard
Maintenant On appelle Rewrite et il choisit si c'est un setoide ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1838 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10anomaly -> errorclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1837 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09MAJ de la MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1836 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1835 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09Backtrack sur le warning Require en Section: trop contraignantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1834 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-06Les tables de coercions ne doivent pas survivre aux sectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1833 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-06la conversion ne doit être testé dans evar_conv qu'en absence de evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1832 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-06has_undefined_isevars était buggéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1831 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-06version 7.0+1 (pour Nicolas Magaud)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1830 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05Avertissement contre les Require dans le corps d'une sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05Interdiction de faire 2 variables de même nom courtherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1828 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05Débogage discharge des coercions; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1827 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05correction bug Omegafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1826 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-04ajout Show Intro(s)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-04message Ambiguous paths seulement si verbosefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1824 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-03Ajout hashconsing universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1823 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-03Depliage des let-in dans le test de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1822 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1821 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1820 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Ajout glob_eq{,T}herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1818 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29Backtracking pour le Matchdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1816 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29traitement du let dans red_product (tactique Red)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1815 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27commit d'un bug de Apply.barras
Avec Apply c, on essaie d'unifier le type de c avec le but courant. Si ca echoue on essaie d'expanser la constante de tete du type du theoreme, et essaie de faire Apply recursivement. Ca ameliore sensiblement la puissance de Apply mais ce n'est pas 100% backward-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1814 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27Reduction du terme preuve fourni par Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1813 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1812 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27Reduction tres significative du terme preuvedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1811 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-26Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous uneclrenard
implication. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1810 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-26Mise a jour des .dependclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1809 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵herbelin
définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1808 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Refine sur les CoFixfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1807 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵herbelin
définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1805 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Bug inférence du prédicat en présence de K-rédexherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1804 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25liste des equiv exporteeclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1802 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Bug dépendances non pertinentes (dû à des K-rédex) dans le type des ↵herbelin
branches des Cases non contournées (bug Solange Coupet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1801 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1800 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts ↵clrenard
générés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1799 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20Normalisation du predicat synthetise pour les Caseclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1798 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20oubli de Elimdep dans le Makefilebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1797 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Un bug corrige.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1796 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Ajouts des theories du paradoxe de Berardidelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1795 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Extension des parametres de Clear + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1794 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Extension des parametres de Cleardelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1793 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-19Oubli Save + je sais plusmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1792 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Ajouts de lemmes (pour Float)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1791 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1790 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-18Interpretation MetaId + Progress + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1789 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:31:46 +0000