aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fichier non traductible (référence à des objets invisibles ce qui empêche...Gravatar herbelin2004-12-09
* Intégré à Implicit.vGravatar herbelin2004-12-09
* Ajout suffixe 8 pour test en nouvelle syntaxeGravatar herbelin2004-12-09
* Plus de statut spécial pour RemarkGravatar herbelin2004-12-09
* VOFILES aussi pour make dependGravatar herbelin2004-12-09
* Désactivation du test du printer arithmétique v7Gravatar herbelin2004-12-09
* travail sur les types extraitsGravatar letouzey2004-12-09
* majGravatar coq2004-12-08
* Ajout bug do_restrict_hypGravatar herbelin2004-12-08
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
* Bugs dans la déclaration du type du terme filtré si non définiGravatar herbelin2004-12-08
* Bug nom exceptionGravatar herbelin2004-12-08
* majGravatar coq2004-12-07
* majGravatar coq2004-12-07
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* The type Pattern.constr_label was isomorphic to Libnames.global_reference.Gravatar sacerdot2004-12-07
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
* Erreur commit précédentGravatar herbelin2004-12-06
* Garder les cast semble décidément le meilleur moyen de rester synchrone ave...Gravatar herbelin2004-12-06
* Suppression des cast après avoir utiliser l'information de type (Tacinv envo...Gravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de RefineGravatar herbelin2004-12-06
* Relâchement obligation d'une contrainte de type sur les Hole en position ter...Gravatar herbelin2004-12-06
* Code mortGravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...Gravatar herbelin2004-12-06
* Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...Gravatar herbelin2004-12-06
* Ajout bug #888Gravatar herbelin2004-12-06
* Ajout bug #889Gravatar herbelin2004-12-06
* C'est trop compliqué de mettre à jour les types du metamap en passant sous ...Gravatar herbelin2004-12-06
* Inutile de réserver les notations à base de '{ }'Gravatar herbelin2004-12-06
* CommentaireGravatar herbelin2004-12-06
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* MAJ affichage nouvelle syntaxeGravatar herbelin2004-12-06
* CommentaireGravatar herbelin2004-12-06
* Bug (cf #892)Gravatar herbelin2004-12-06
* MAJGravatar herbelin2004-12-05
* MAJ changements ChoiceFactsGravatar herbelin2004-12-05
* MAJGravatar herbelin2004-12-05
* Paramétrisation du domaine des axiomes de choix + ajout description = choice...Gravatar herbelin2004-12-05
* Bug 'set n in * |-'Gravatar herbelin2004-12-04
* Failed in 8.0pl1Gravatar herbelin2004-12-04
* Orthographe!Gravatar herbelin2004-12-03
* Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...Gravatar herbelin2004-12-03
* Was failing in 8.0pl1Gravatar herbelin2004-12-03
* Amélioration message d'erreur v8Gravatar herbelin2004-12-03
* pp of nested fixpoints (dangling with/for)Gravatar barras2004-12-01
* Export pr_intro_patternGravatar herbelin2004-11-30
* UserError in reduce_to_*_refGravatar herbelin2004-11-29
* Complétion commit précédentGravatar herbelin2004-11-29
* *** empty log message ***Gravatar gregoire2004-11-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:01:16 +0000