aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-11Bug collision entre les implicites d'un global et les variables locales de mÃ...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 01:52:06 +0000