aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-09-02Bug traduction Search, SearchPattern, etc.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4290 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Plus de passage du scope tmp sous les lambdasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4289 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-01Passage de 'relation' à Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4288 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4287 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Syntaxe des constructeurs et des hypothesesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4286 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Bug et améliorations diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4285 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31'Assumptions' sur le modèle général des lieursherbelin
Syntaxe à la ML pour les constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4284 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Symetrisation des changements implicites de scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4283 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ↵herbelin
| S (n:nat)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4282 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Affichage des inductifs en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4281 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4280 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4278 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4277 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Fusion -translate et -ftranslateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Traducteur de correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4275 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4274 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Traduction mlnamesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4273 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Pb de mot-cleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4272 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Amélioration affichage syntaxe modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4271 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Positionnement precoce de l'option -v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4270 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Ajout token '!' pour correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4269 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Enregistrement tuple_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4268 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Notation access au dessous du niveau applicatif (2eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4267 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-13Hack pour ajouter Proof apres Correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4266 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-13Notation access au dessous du niveau applicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4265 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug et améliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug et amliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug détypage du fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4262 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4261 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Ajout LetTupleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4260 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Mémo nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4259 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4258 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Option -v8 à coqtop lance coqtopnewherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4256 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4255 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4254 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4253 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Outils de traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4252 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Ajout option_fold_rightherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4251 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Affichage {}+{}, niveau paire au plus hautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4250 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Un peu d'aide pour le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4249 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-06Ajout de l'opti des fermeture (mais debranche pour l'instant)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4248 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-05Improved reduction machine with closure: should use less memorybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4247 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-24Bug globalisation Grammar (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4246 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4244 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-23Bug globalisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4242 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-18coqide: new search and AutoCompletionmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4240 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4239 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4238 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-16coqide: fixed problems with -R -I and coqide interactionmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4237 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:37:49 +0000