aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-09-09Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la ↵herbelin
résolution des implicites restant après interprétation des termes dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7363 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Conséquences nettoyage pretyping.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7362 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ↵herbelin
ltac pour qu'il retourne les evar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7361 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Suppression code inactif et commentaire apparemment incorrect (pour éviter ↵herbelin
confusions suite à question de CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7360 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Suppression test CCSolve car remplaçé par Congruence mais qui ne traite ↵herbelin
pas les connecteurs propositionnels (pour Pierre C.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7359 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7357 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Test clear final dans intros patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7356 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ↵herbelin
'_' donnés dans le 'intros' (à cause des dépendances potentielles) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7355 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Simplification message d'anomalieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7352 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-08Réparation bug #1004; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7351 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7349 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7347 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-06Un vieux bug d'affichage des lieurs (cf bug #1005)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7346 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7343 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7341 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7339 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7337 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7335 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7333 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7331 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7329 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7327 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7325 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7323 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-26*** empty log message ***letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7322 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7320 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7318 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7316 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7314 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-22argument inutilisé de zip: toujours l'identitéletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7313 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7311 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7309 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7307 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7303 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-18code cleaning. No changes as far as tested.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7302 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7300 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7299 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-17new congruencecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7296 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7294 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7292 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7290 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7288 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7286 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7284 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7282 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7280 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7278 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:45:30 +0000