aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-01-16Bugs affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Subst sur une hyp qui n'existe pas ne fait pas une anomaliebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3515 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Ajout de RComputedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3514 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Ajout de la tactique Supdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3513 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3512 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16renommage de TAF.v en MVT.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16-emacs: plus de prompt entre les lignesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3510 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Correction d'un petit bug dans Sup0desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3509 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de RealsB en Rbasedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de Rbase.v en RIneq.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3507 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3506 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Problème de désynchronisation des variables du type et du corps d'un ↵herbelin
point-fixe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3504 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3503 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Bug en présence de let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3502 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Bug en présence de let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3498 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-13patch configure (V Aymeric)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3496 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3495 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09correction de bug de Subst: ne faisait rien lorsque l'hypothesebarras
n'apparaissait que dans le but... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3493 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3492 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-07Retour printer ast pour V7.4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3491 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3490 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-06SearchAboutfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-06bit vectorsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-31Amélioration règles d'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3487 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-30Commentaires; optimisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3486 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-30Amélioration choix des noms dans abstract_list_allherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3485 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-28Prise en compte notations dans les extensions de motiffherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3484 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-24Utilisation du second-ordre avec possibilité de K-rédex dans lemInvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3482 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-24code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-23Re-essai de forcer le terme réécrit à apparaître dans le butherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3480 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-23Tentative d'interdire les K-abstractions si allow_K est faux et leherbelin
motif n'a pas de métas (dans unify_to_subterm_list) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3479 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-23Prise en compte application partielle dans dependentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3477 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-22Cas motif universelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3476 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationherbelin
faite par Rewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Affinement affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3473 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3472 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Affinement affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Plus de notation cablees dans 'annot'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3470 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3469 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-20Prise en compte des coercions dans les 'with' bindingsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3468 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3464 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19suppression de l'archive cvs d'un bout de debugletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3462 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:32:57 +0000