aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-05-23coqide: blaster 2monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4071 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23fabrication de ide/utf8.voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4070 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23Bug en mode translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4069 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4068 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23coqide: blaster 2monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4067 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4066 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4065 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Ajout V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4064 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ↵herbelin
inefficacité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4063 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Test backtrackingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4062 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Ajout V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Preservation affichage des ?n en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22coqide: blaster V1monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Ocaml 3.00 a existe'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4058 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22compat windowsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4057 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4056 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4055 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notations ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4053 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4051 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Nouveaux testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4048 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4047 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4046 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4044 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ↵herbelin
points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4041 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20CoqIde: externalsmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Prise en compte notation dans Inductif pour traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4039 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20command_windows fixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4038 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Extension renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4037 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4036 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Affichage METAherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4035 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructutation Hipattern Patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4034 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
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
2003-05-19Restructuration des procédures de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4031 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19CoqIde : but reset_modfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4030 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 15:10:56 +0000