aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-09-06Pour accomoder autant le printer v8 que v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4315 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Protection contre les types sans corps associéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4314 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4313 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4311 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4310 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05principes de récurrences plus efficaces pour l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4309 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4308 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Zabs_Zsgnletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4307 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05highlighting de Extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4306 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05bug dans calcul nb d'occurrencesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4305 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05affichage de la nature des colonnesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4304 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05install coqwcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4303 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05coqwcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4302 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Impression sans ',' des constructeurs de meme type, pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4301 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03option pour supprimer les menus contextuels sur les butsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4299 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4298 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4297 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4296 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Relachement conflit 'with' dans le cas des Module with Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4295 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Contorsions pour que l'interpretation deses foncteurs depende des parametres ↵herbelin
de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4294 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:05:00 +0000