aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-06-10Simplification case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Record; raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4123 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4122 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Globalisation des tactiques avant traduction pour capture des noms; ↵herbelin
affinement divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4121 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Distinction mode v7 ou translate; conséquences du déplacement traducteur ↵herbelin
de nom dans Constrextern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4120 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement de code dans command; MAJ DebugOnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4119 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Mise en place structure pour des 'arguments scope' dirigés par une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4118 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs Extension du traducteur de nom Ajout notation c.(f) en v8 pour les projections de Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4117 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Passage des noms de tactiques à kernel_name pour compatibilité avec les ↵herbelin
foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Factorisation de detype_case pour utilisation par l'afficheur de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4113 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Traducteur + passage des noms de tactiques à kernel_name pour ↵herbelin
compatibilité avec les foncteurs + réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4112 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵herbelin
de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4111 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Extension de Locate sur les symboles avec recherche de sous-chaînes; mise ↵herbelin
en place structure pour des 'arguments scope' dirigés par une classe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4109 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Globalisation de ce qui n'etait pas encore globaliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4108 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout fonctions de recherche de sous-chaines (merci a Jacek)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4105 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08interaction entre fun/case permut et assert falseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4104 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06coqide: compile sans activate reparemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06bug CoqIDE avec Goalfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4101 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-06Added new syntax definitionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-04bugfix for Ground ( merci JC )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4097 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-04Ground update + some bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4096 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-02 au lieu de makemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4095 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-30oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4094 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4093 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4092 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29niveau 49 devient nextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4091 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Ground daily updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4090 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29niveau 49 devient nextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4089 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4088 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29:= dans un record engendre un LetIn qui n'etait pas géréletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4087 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-28gestion plus fine des beta-redex lineaires (cf nb_occur_match)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4085 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-27'only parsing' pour le passage de trucT a trucherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4084 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4083 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26coqide: blaster interruptiblemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4082 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4081 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26GIntuition now matches Intuition up to hyps renaming.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4080 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26Added breakpoint in Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4079 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4077 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26configure pour CoqIde reparemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4076 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-25Ground and CCsolve updatescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Realsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4074 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ↵herbelin
ajout FreshId git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4073 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24Ajout FreshIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:03:25 +0000