aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* backtrack unification types et deplacement make_clenv_bindingGravatar filliatr2001-03-01
* introduction d'un refine avec resolution des types et de l'instantiation des ...Gravatar mohring2001-02-28
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Obsolète (cf Coqlib)Gravatar herbelin2001-02-14
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* exporting traverse_to and mutate: they are used in pcoq.Gravatar bertot2001-02-08
* Reparation du pretty-print pour les tactiquesGravatar delahaye2001-02-07
* Correction pour les Unfold/Fold dans CbvGravatar delahaye2001-02-06
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* *** empty log message ***Gravatar mohring2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* make docGravatar herbelin2001-01-27
* Retour en arrière sur le pb f_equal en attente meilleure solutionGravatar herbelin2001-01-22
* Bug « f_equal » : arguments inférables par une unification des types qui n...Gravatar herbelin2001-01-21
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Elimination des coupuresGravatar herbelin2000-12-26
* Remplacement de debug en assertGravatar herbelin2000-12-25
* Code mortGravatar herbelin2000-12-20
* Bug dans l'utilisation de l'option debugGravatar herbelin2000-12-20
* Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...Gravatar herbelin2000-12-20
* Ajout set_lcGravatar herbelin2000-12-20
* Correction pour les variables abstraites dans les Tactic DefinitionsGravatar delahaye2000-12-19
* Code mortGravatar herbelin2000-12-18
* DocumentationGravatar herbelin2000-12-18
* Redondant or incompatible instantiations in clenv_assign now correctly trappedGravatar herbelin2000-12-16
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Ajout erreur DoesNotOccurInGravatar herbelin2000-12-06
* Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...Gravatar herbelin2000-12-05
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Elimination du 'Gravatar delahaye2000-11-28
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...Gravatar herbelin2000-11-27
* Branchement du mécanisme d'instantiation des Evar en présence de définitio...Gravatar herbelin2000-11-27
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Correction d'un bug lorsque des Variables sont clearees dans le but courantGravatar delahaye2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Affichage des paths avec des '.', 2eme; prise en compte qualidGravatar herbelin2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* NettoyageGravatar herbelin2000-11-22
* Tout est deja traite dans TacinterpGravatar delahaye2000-11-21
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Prise en compte noms longsGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 03:45:43 +0000