aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2001-09-17unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesbarras
2001-09-14exceptionsbarras
2001-09-10Un conv aurait dû être un conv_leqherbelin
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-09-09Suppression du retypage dans w_Declareherbelin
2001-08-10Parsingherbelin
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-08-05Code mortherbelin
2001-07-24Suppression de l'affichage du non-reparsable 'Local constraint change'herbelin
2001-07-19Changements dans le traitement des qualid'sdelahaye
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
2001-06-29Backtracking pour le Matchdelahaye
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-05-28Pretty -> Prettypfilliatr
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-18Erreur dans un commentaire ...clrenard
2001-05-07quelques bug reports mineursbarras
2001-05-03Changement de la structure des points fixesbarras
2001-04-19Metas dans les Unfold'sdelahaye
2001-04-14Reparation du bug de Trydelahaye
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-04-03utilisation de Options.if_verbosefilliatr
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ...filliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
2001-02-28introduction d'un refine avec resolution des types et de l'instantiation des ...mohring
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
2001-02-14Obsolète (cf Coqlib)herbelin
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans certains...filliatr
2001-02-08exporting traverse_to and mutate: they are used in pcoq.bertot
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-02-06Correction pour les Unfold/Fold dans Cbvdelahaye
2001-02-01application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésfilliatr
2001-02-01*** empty log message ***mohring
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-27make docherbelin
2001-01-22Retour en arrière sur le pb f_equal en attente meilleure solutionherbelin
2001-01-21Bug « f_equal » : arguments inférables par une unification des types qui n...herbelin
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-26Elimination des coupuresherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 08:06:03 +0000