aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-10nat_scope ouvert par defautherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10type_scopeherbelin
2003-10-10Suppression de definitions equivalentesherbelin
2003-10-10Bug undoherbelin
2003-10-10Notation '^'herbelin
2003-10-10*** empty log message ***herbelin
2003-10-10Plus d'Eval Computeherbelin
2003-10-10MAJ commentairesherbelin
2003-10-10MAJherbelin
2003-10-10Typoherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-10-10Cablage en dur de inversionherbelin
2003-10-10code mortherbelin
2003-10-10show_subgoals dans Pfeditherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 21:58:00 +0000