aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...Gravatar herbelin2000-11-27
* Affichage des définitions localesGravatar herbelin2000-11-27
* Ajout map_constr_with_full_binders et strong pour SimplGravatar herbelin2000-11-27
* Changement du parseur par défaut dans SyntaxGravatar herbelin2000-11-27
* Généralisation de constant_opt_value en reference_opt_valueGravatar herbelin2000-11-27
* Branchement du mécanisme d'instantiation des Evar en présence de définitio...Gravatar herbelin2000-11-27
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* Bug dans le calcul des dépendances dans add_discharged_constantGravatar herbelin2000-11-27
* NettoyageGravatar herbelin2000-11-26
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* Le nouvel Induction s'appelle NewInductionGravatar herbelin2000-11-26
* MAJGravatar herbelin2000-11-26
* Prise en compte qualidGravatar herbelin2000-11-26
* Restruration autour de qualidargGravatar herbelin2000-11-26
* Calcul du chemin optimal dans qualid_of_globalGravatar herbelin2000-11-26
* Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...Gravatar herbelin2000-11-26
* Prise en compte noms longs dans divers fonctions de PrintGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametab + nettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
* Remplacement de certains sp_of_id par des locateGravatar herbelin2000-11-26
* sp au lieu de id dans END-SECTIONGravatar herbelin2000-11-26
* MAJGravatar herbelin2000-11-24
* Bug relocation des hypothèses quand les contextes de définitions et d'utili...Gravatar herbelin2000-11-24
* Réorganisation autour de globalize_constrGravatar herbelin2000-11-24
* NettoyageGravatar herbelin2000-11-24
* Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...Gravatar herbelin2000-11-24
* Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'Gravatar herbelin2000-11-24
* MAJGravatar filliatr2000-11-24
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* Ajout BEST partout a coqcGravatar filliatr2000-11-24
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* resolution implicites dans produits (bug)Gravatar filliatr2000-11-24
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 04:37:03 +0000