aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* MAJGravatar herbelin2000-11-24
* synchronisation RequireGravatar filliatr2000-11-24
* - coqc: utilise le meilleur coq possibleGravatar filliatr2000-11-24
* Petite simplif due au nouveau TautoGravatar delahaye2000-11-24
* Nouveau choix pour l'intros initialGravatar delahaye2000-11-24
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* On n'introduit que des produits non dependantsGravatar delahaye2000-11-23
* Correction d'un bug lorsque des Variables sont clearees dans le but courantGravatar delahaye2000-11-23
* Affichage des QUALIDGravatar herbelin2000-11-23
* Simplification de l'accès aux globauxGravatar herbelin2000-11-23
* Search réparéGravatar filliatr2000-11-23
* MAJGravatar herbelin2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spGravatar herbelin2000-11-23
* id_of_global devient sp_of_globalGravatar herbelin2000-11-23
* Fonction qualid_of_global pour affichage des paths avec des '.'Gravatar herbelin2000-11-23
* Affichage des paths avec des '.', 2eme; prise en compte qualidGravatar herbelin2000-11-23
* Informations inutilesGravatar herbelin2000-11-23
* Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;Gravatar herbelin2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Ajout push_rels_assumGravatar herbelin2000-11-23
* Bug qualidconstarg (intervient pour Transparent)Gravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* NettoyageGravatar herbelin2000-11-22
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* Reparation bug mutuels indGravatar mohring2000-11-22
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
* Tout est deja traite dans TacinterpGravatar delahaye2000-11-21
* Elimination d'un test sur les macrosGravatar delahaye2000-11-21
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Ajout d'une fonction pour recuperer la liste des constantesGravatar delahaye2000-11-21
* Ajout du clean pour tolink.mlGravatar delahaye2000-11-21
* reset_name: try / with juste autour de find_entry_p (=> propage lesGravatar filliatr2000-11-21
* ln -sf au lieu de ln -sGravatar filliatr2000-11-21
* ajout d'un frozen_state après la fermeture d'une section (sinon bug !)Gravatar filliatr2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* PatternMatchingFailure n'etait pas rattrapeeGravatar herbelin2000-11-21
* NettoyageGravatar herbelin2000-11-21
* Bugs make_tuple et existS_patternGravatar herbelin2000-11-21
* MAJGravatar herbelin2000-11-21
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
* Begin-End Silent deviennent Set?Unset SilentGravatar mohring2000-11-21
* correction bug ResetGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* XML débranchéGravatar filliatr2000-11-21
* Prise en compte des implicites dans les regles de grammairesGravatar herbelin2000-11-21
* Petit bug entre close_section'sGravatar herbelin2000-11-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 23:32:47 +0000