aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2000-12-25Alias variable_pathherbelin
2000-12-25Effet réorganisation Classopsherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-25Bug vieux Matchherbelin
2000-12-25Bug prédicatherbelin
2000-12-25Traducteur automatique de scripts vernacherbelin
2000-12-22*** empty log message ***mayero
2000-12-22Typoherbelin
2000-12-22MAJherbelin
2000-12-22cleanallherbelin
2000-12-22Insertion COQPATHPREFIX pour isntallation localeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 20:00:44 +0000