aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵herbelin
interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵herbelin
interp et déclarations des scopes d'argument dans Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4364 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Activation déclaration automatique de scope d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4363 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare et déclarations des scopes d'argument dans Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4362 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Mise en place affichage spécifique pour le scope des typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4361 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Scope type pour le codomaine de Prod aussi; ajout extern_rawtypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4360 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Scope type pour le codomaine de Prod aussiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4359 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4358 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; Mise en place affichage ↵herbelin
spécifique pour le scope des types; 'Delimits' -> 'Delimit' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4357 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12open superfluherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4356 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Simplification vis a vis de Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4355 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Branchement constant sur Coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4354 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4352 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4351 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Renommage des variables '_'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4350 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Passage des projections au niveau 1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-109 est associatif a gaucheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4348 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Debranchement du traducteur pour Load !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4347 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10warning vers std_errherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4346 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Bug predicat old Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4345 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Traduction de Distfixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4344 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10typonarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4343 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Ajout 'mod' comme keywordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4342 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Oubli des guillemets dans Commentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4341 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Pretty-pretting fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4340 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4339 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Bug predicat let-tupleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4338 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4337 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Traduction des réferences arguments de commandes non primitives; 'Grammar ↵herbelin
tactic' devient 'Tactic Notation' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4335 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09'Grammar tactic' devient 'Tactic Notation'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4334 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; synchro avec constrexternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4333 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; renommage de l'ident '_'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4332 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4331 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; protection contre clash dans return_typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4330 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4329 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4328 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Protection traducteur contre meta de Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4327 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4326 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4325 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
records en v7 aussi git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4324 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Check local definitions in context of inductive typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4323 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06'Implicits qid' -> 'Implicit Arguments qid'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4320 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4318 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Adapter l'entree de grammaire a la version 7 ou 8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4317 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:52:37 +0000