aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2001-06-16code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1788 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-15Fix d'un bug de Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1787 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-13plus besoin de separer les ?barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1786 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-13Prise en compte env local (et defs locales) dans Changeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1785 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes ↵clrenard
automatiquement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1784 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout des entrees puor Setoid_replace.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout de la tactique Setoid_replace.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1782 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 03:44:09 +0000