aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* Ground updateGravatar corbinea2003-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4193 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground Update.Gravatar corbinea2003-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground updateGravatar corbinea2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4171 85f007b7-540e-0410-9357-904b9bb8a0f7
* ground updateGravatar corbinea2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground major update ... mmm, sounds exciting !Gravatar corbinea2003-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
* ground updateGravatar corbinea2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major Ground update, may break semanticsGravatar corbinea2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground updateGravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update, new files.Gravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update.Gravatar corbinea2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4144 85f007b7-540e-0410-9357-904b9bb8a0f7
* enieme correction du nommage modulaireGravatar letouzey2003-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4143 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin de l'affichage des signatures de modules dans les *.mlGravatar letouzey2003-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4142 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵Gravatar herbelin2003-06-10
| | | | | | de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation de ce qui n'etait pas encore globaliseGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4108 85f007b7-540e-0410-9357-904b9bb8a0f7
* interaction entre fun/case permut et assert falseGravatar letouzey2003-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4104 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugfix for Ground ( merci JC )Gravatar corbinea2003-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update + some bugfixGravatar corbinea2003-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4096 85f007b7-540e-0410-9357-904b9bb8a0f7
* oupsGravatar letouzey2003-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground daily updateGravatar corbinea2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4090 85f007b7-540e-0410-9357-904b9bb8a0f7
* := dans un record engendre un LetIn qui n'etait pas géréGravatar letouzey2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4087 85f007b7-540e-0410-9357-904b9bb8a0f7
* gestion plus fine des beta-redex lineaires (cf nb_occur_match)Gravatar letouzey2003-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4085 85f007b7-540e-0410-9357-904b9bb8a0f7
* GIntuition now matches Intuition up to hyps renaming.Gravatar corbinea2003-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added breakpoint in Ground tactic.Gravatar corbinea2003-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4079 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved engine.ml4 to ground.ml4, added option 'Ground Depth'Gravatar corbinea2003-05-26
| | | | | | | fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground and CCsolve updatesGravatar corbinea2003-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformite de la precedence du '-' unaire avec celle de Notations ↵Gravatar herbelin2003-05-21
| | | | | | (suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformite de la precedence du '-' unaire avec celle de NotationsGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformite de la precedence du '-' unaire avec celle de NotationsGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major Ground tactic update, sensible performance improvementGravatar corbinea2003-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations arithmetiquesGravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4008 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugfixes in Ground.Gravatar corbinea2003-05-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enhancement of the Ground tactic, addition of GTauto and GIntuition.Gravatar corbinea2003-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation erreurs TacAlias; Globalisation moins tolérante dans lesGravatar herbelin2003-04-28
| | | | | | | définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug concernant les projecteurs de Record avec args logiquesGravatar letouzey2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3967 85f007b7-540e-0410-9357-904b9bb8a0f7
* adaptation a Acc_iterGravatar letouzey2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3965 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugfix in Ground tacticGravatar corbinea2003-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the Ground tactic.Gravatar corbinea2003-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
| | | | | | | Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 03:14:30 +0000