aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-09-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7384 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-16changed the syntax categories of arguments of functional schemecoq
(constr --> ident). Transparent for the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7383 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7381 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7379 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7377 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7375 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7373 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7371 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-10Petit bug Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7370 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7368 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7367 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7366 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7365 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Référence pour IntMapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7364 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:51:19 +0000