aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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
2000-12-25Remplacement de debug en assertherbelin
2000-12-20Code mortherbelin
2000-12-20Bug dans l'utilisation de l'option debugherbelin
2000-12-20Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...herbelin
2000-12-20Ajout set_lcherbelin
2000-12-19Correction pour les variables abstraites dans les Tactic Definitionsdelahaye
2000-12-18Code mortherbelin
2000-12-18Documentationherbelin
2000-12-16Redondant or incompatible instantiations in clenv_assign now correctly trappedherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-12Hint Unfold Local + commentairesmohring
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-12-05Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...herbelin
2000-12-02Portage d'AutoRewritedelahaye
2000-11-28Elimination du 'delahaye
2000-11-27Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...herbelin
2000-11-27Branchement du mécanisme d'instantiation des Evar en présence de définitio...herbelin
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-23Correction d'un bug lorsque des Variables sont clearees dans le but courantdelahaye
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-23Affichage des paths avec des '.', 2eme; prise en compte qualidherbelin
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-23Reparation IsMutConstruct + Transparentmohring
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-22Nettoyageherbelin
2000-11-21Tout est deja traite dans Tacinterpdelahaye
2000-11-21Traitement du pretty-print des Redexpdelahaye
2000-11-20Prise en compte noms longsherbelin
2000-11-15methode exportfilliatr
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:05:07 +0000