aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-01-17MAJherbelin
2001-01-15Essai d'axiomatisation des numeralmohring
2001-01-15Ajout de commentaire coqwebmohring
2001-01-15Raffinementsherbelin
2001-01-14Petit bug encoreherbelin
2001-01-14Bien sûr: bugs sur précédent commit; améliorationsherbelin
2001-01-14Prise en compte de l'allocation mémoire et affichage des résultats net du s...herbelin
2001-01-12Now Ring does not perform any more the same reduction twice.sacerdot
2001-01-12Comment fixedsacerdot
2001-01-11corr bug -mayero
2001-01-11Now reduction to normal form is done only when the term is notsacerdot
2001-01-11Many unuseful rewritings are no more done by Ring.sacerdot
2001-01-11Bug environnementherbelin
2001-01-11Mise a jour Rbasemohring
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Tactic Definition -> Meta Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2001-01-04Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...herbelin
2001-01-03Prise en compte des ??herbelin
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-27Améliorationsherbelin
2000-12-27Bug installation non localeherbelin
2000-12-26MAJherbelin
2000-12-26Dernière MAJherbelin
2000-12-26MAJherbelin
2000-12-26Bug de contextesherbelin
2000-12-26MAJherbelin
2000-12-26Elimination des coupuresherbelin
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...herbelin
2000-12-26On n'évite plus les globaux dans Intro, mais on les évite dans Abstractherbelin
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin
2000-12-26Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der...herbelin
2000-12-26MAJherbelin
2000-12-25Command -> Constrherbelin
2000-12-25Retrait du test d'existence "is_global" dans Intro ( fresh_id ) dherbelin
2000-12-25Normalisation betaiota du pattern avant enregistrement comme hint (certains d...herbelin
2000-12-25bug head_pattern_boundherbelin
2000-12-25Modifs sur le langage de tactiques et pas de "ë" dans Micaeladelahaye
2000-12-25Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifsdelahaye
2000-12-25Bug confusion existS/sigSherbelin
2000-12-25Token n'est plus un keywordherbelin
2000-12-25Command -> Constrherbelin
2000-12-25MAJherbelin
2000-12-25Remplacement de debug en assertherbelin
2000-12-25Bug discharge process_classherbelin
2000-12-25find_section_variable : un traducteur id -> sp pour variables de section; var...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 02:59:09 +0000