aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* majGravatar coq2005-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6879 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6877 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de l'axiome du but prouve par la tactique simplifiGravatar coq2005-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Unset Implicit Arguments manquantGravatar herbelin2005-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug de dependent_hyps qui ne met pas à jour le type des hyps ↵Gravatar herbelin2005-03-20
| | | | | | dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵Gravatar herbelin2005-03-20
| | | | | | hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6865 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction erreur grossière de non restauration d'état en cas de retour ↵Gravatar herbelin2005-03-19
| | | | | | exceptionnel; suppression without_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le type d'un Let est considéré comme 'user-provided' par le noyau et doit ↵Gravatar herbelin2005-03-19
| | | | | | donc avoir des univers frais git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug #935Gravatar herbelin2005-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report depuis la V8.0pl2 de la correction d'un bug du traducteurGravatar herbelin2005-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6858 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6856 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6855 85f007b7-540e-0410-9357-904b9bb8a0f7
* appel de Simplify depuis CoqGravatar coq2005-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6852 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6850 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6849 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6848 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6846 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6845 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ PolyList -> ListGravatar herbelin2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6843 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelles tactiques pour appeler des procedures de decision du premier ordreGravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6841 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6839 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unsharing before exportation to ensure uniqueness of xml id'sGravatar herbelin2005-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la substitution combinée avec l'instanciation en réponse à ↵Gravatar herbelin2005-03-15
| | | | | | 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
* majGravatar coq2005-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6834 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6832 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6830 85f007b7-540e-0410-9357-904b9bb8a0f7
* Explicitation d'un nom de variable nécessaire au bon typage, suite à ↵Gravatar herbelin2005-03-12
| | | | | | suppression des _ du contexte des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6829 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack version 1.82 awaiting for better understanding of the consequences ↵Gravatar herbelin2005-03-12
| | | | | | of removing Anonymous from evars contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6828 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Méthode plus raisonnable pour supprimer l'inefficacité des evars ↵Gravatar herbelin2005-03-11
| | | | | | dépendantes de Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de COQLIB/user-contrib à l'installation pour insister sur la ↵Gravatar herbelin2005-03-11
| | | | | | possibilité qu'il est utilisable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargementGravatar herbelin2005-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6823 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6821 85f007b7-540e-0410-9357-904b9bb8a0f7
* A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵Gravatar herbelin2005-03-10
| | | | | | optimisée pour le prétypage qui normalise les evars à la volée (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6820 85f007b7-540e-0410-9357-904b9bb8a0f7
* A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵Gravatar herbelin2005-03-10
| | | | | | optimisée pour le prétypage que normalise les evars (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6819 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6817 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #931 (continued): no recursion on the evars instantiationGravatar herbelin2005-03-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6816 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6814 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:22:53 +0000