aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-10MAJ .v8herbelin
2003-10-10pf_get_new_id en provenance de feu wcclausenvherbelin
2003-10-10Suppression clenv_change_head que seul Wcclausenv utisaitherbelin
2003-10-10Dead of 'a somewhat cryptic module'herbelin
2003-10-10Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...herbelin
2003-10-10Ajout printers pour constr et constr_pattern (sans traduction)herbelin
2003-10-10Unification lemInv et lemInv_inherbelin
2003-10-10pr_tactic sans traduction; affichage Inversionherbelin
2003-10-10Cablage en dur de inversionherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-10-10Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à c...herbelin
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiquesherbelin
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...herbelin
2003-10-10Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...herbelin
2003-10-10Gestion en temps constant de la pile des Unfoherbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-10Cacher les .v8herbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-09Nouveau format de l'option 'format'herbelin
2003-10-09Compatibilite ocaml 3.06 et 3.07herbelin
2003-10-09Syntaxe VernacEndProof changee pour ajout mot-cle 'Admitted'herbelin
2003-10-08Teste interaction ltac et modulesherbelin
2003-10-08Ajout exemple parametres implicitesherbelin
2003-10-08Bug utilisation nametab pour ltacherbelin
2003-10-08Pb residuel avec la prise en compte des parametres implicites d'inductifsherbelin
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ...herbelin
2003-10-08Des abbreviations pour constrintern.ml; generic argument IdentArgherbelin
2003-10-08Des abbreviations pour constrintern.mlherbelin
2003-10-08Test Conjectureherbelin
2003-10-08MAJherbelin
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...herbelin
2003-10-08Renommage no-strict en -strict-implicitherbelin
2003-10-08Renommage no-strict en -strict-implicitherbelin
2003-10-08Renommage no-strict en -strict-implicit; option -dont-load-proofsherbelin
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
2003-10-07majfilliatr
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop com...herbelin
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
2003-10-06Pour rendre make un peu moins verbeuxletouzey
2003-10-06NEWCONTRIBVO doit apparaitre apres CONTRIBVOherbelin
2003-10-06pour ocamlwebletouzey
2003-10-06distinguer interp_cs et interp_setcsletouzey
2003-10-04Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand new...herbelin
2003-10-04Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)herbelin
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
2003-10-04majfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 15:42:59 +0000