aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Essai d'axiomatisation des numeralGravatar mohring2001-01-15
* Ajout de commentaire coqwebGravatar mohring2001-01-15
* RaffinementsGravatar herbelin2001-01-15
* Petit bug encoreGravatar herbelin2001-01-14
* Bien sûr: bugs sur précédent commit; améliorationsGravatar herbelin2001-01-14
* Prise en compte de l'allocation mémoire et affichage des résultats net du s...Gravatar herbelin2001-01-14
* Now Ring does not perform any more the same reduction twice.Gravatar sacerdot2001-01-12
* Comment fixedGravatar sacerdot2001-01-12
* corr bug -Gravatar mayero2001-01-11
* Now reduction to normal form is done only when the term is notGravatar sacerdot2001-01-11
* Many unuseful rewritings are no more done by Ring.Gravatar sacerdot2001-01-11
* Bug environnementGravatar herbelin2001-01-11
* Mise a jour RbaseGravatar mohring2001-01-11
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Tactic Definition -> Meta DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...Gravatar herbelin2001-01-04
* Prise en compte des ??Gravatar herbelin2001-01-03
* Let doit etre utilise dans le mode de preuveGravatar delahaye2001-01-03
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* AméliorationsGravatar herbelin2000-12-27
* Bug installation non localeGravatar herbelin2000-12-27
* MAJGravatar herbelin2000-12-26
* Dernière MAJGravatar herbelin2000-12-26
* MAJGravatar herbelin2000-12-26
* Bug de contextesGravatar herbelin2000-12-26
* MAJGravatar herbelin2000-12-26
* Elimination des coupuresGravatar herbelin2000-12-26
* Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...Gravatar herbelin2000-12-26
* On n'évite plus les globaux dans Intro, mais on les évite dans AbstractGravatar herbelin2000-12-26
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
* Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der...Gravatar herbelin2000-12-26
* MAJGravatar herbelin2000-12-26
* Command -> ConstrGravatar herbelin2000-12-25
* Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dGravatar herbelin2000-12-25
* Normalisation betaiota du pattern avant enregistrement comme hint (certains d...Gravatar herbelin2000-12-25
* bug head_pattern_boundGravatar herbelin2000-12-25
* Modifs sur le langage de tactiques et pas de "ë" dans MicaelaGravatar delahaye2000-12-25
* Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifsGravatar delahaye2000-12-25
* Bug confusion existS/sigSGravatar herbelin2000-12-25
* Token n'est plus un keywordGravatar herbelin2000-12-25
* Command -> ConstrGravatar herbelin2000-12-25
* MAJGravatar herbelin2000-12-25
* Remplacement de debug en assertGravatar herbelin2000-12-25
* Bug discharge process_classGravatar herbelin2000-12-25
* find_section_variable : un traducteur id -> sp pour variables de section; var...Gravatar herbelin2000-12-25
* Alias variable_pathGravatar herbelin2000-12-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:55:42 +0000