aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2001-09-24Marre des unrecognized objectsherbelin
2001-09-21Réparation des options Set Printing and coherbelin
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
2001-09-20Amélioration affichage de print_leaf_entryherbelin
2001-09-20Rajout 'Set Printing Depth'herbelin
2001-09-20Transparentbarras
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...herbelin
2001-09-14Search prenait en compte le contenu des sections alors que celui-ci n'existe ...herbelin
2001-09-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
2001-09-14Ajout syntaxe "Assert H:T."herbelin
2001-09-13Prise en compte qualid dans Hint Unfoldherbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
2001-09-06Rétablissement de Print Sectionherbelin
2001-08-28Remplace numarg -> pure_numarg dans Double Inductionmohring
2001-08-13bug incompatibilitéherbelin
2001-08-10Pour contourner un bug de camlp4 3.02herbelin
2001-08-10Parsingherbelin
2001-08-08Renommage TrueCut -> Assertherbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-08-06Nouvelle entrée ident_or_numargherbelin
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
2001-07-19Changements dans le traitement des qualid'sdelahaye
2001-07-19modifs de preuves (plus simples)mayero
2001-07-13reparation regles pour parsing Coercion Localmohring
2001-07-04ajout Show Intro(s)letouzey
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Ajout glob_eq{,T}herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
2001-05-29Retablissement de minicoqcoq
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-28Pretty -> Prettypfilliatr
2001-05-03Changement de la structure des points fixesbarras
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
2001-04-25Amelioration affichageherbelin
2001-04-24Messages d'erreur Casesherbelin
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
2001-04-23un warning pas beau supprimméfilliatr
2001-04-20Petit menagedelahaye
2001-04-19*** empty log message ***mayero
2001-04-19Essais dans Ltacdelahaye
2001-04-15Bug affichage d'implicites pour les vars lieesherbelin
2001-04-14Non parenthesage des applications de tactiquesdelahaye
2001-04-12Ajout de _ dans les patterns d'intromohring
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 12:17:57 +0000