aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-03-02majcoq
2005-03-01majcoq
2005-03-01clean de parser.optherbelin
2005-03-01Code mortherbelin
2005-03-01MAJherbelin
2005-02-28majcoq
2005-02-27majcoq
2005-02-26majcoq
2005-02-25majcoq
2005-02-24majcoq
2005-02-23majcoq
2005-02-23quelques tactics ltacletouzey
2005-02-22majcoq
2005-02-22Suppression des fichiers temporairesherbelin
2005-02-21majcoq
2005-02-21majcoq
2005-02-21*** empty log message ***herbelin
2005-02-21Pas de dépendance en Omegaherbelin
2005-02-21Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueherbelin
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
2005-02-21- Correction de bugsherbelin
2005-02-20majcoq
2005-02-20Keep ClosedSection marker for resetherbelin
2005-02-19majcoq
2005-02-18majcoq
2005-02-18majcoq
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_functionherbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...herbelin
2005-02-18Standardisation of function names about structuresherbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Déboggueur et code mortherbelin
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Ajout it_mkNamedProd_wo_LetInherbelin
2005-02-18Ajout splay_lambdaherbelin
2005-02-18Code mortherbelin
2005-02-18Added map_named_contextherbelin
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
2005-02-18Ajout constant printerherbelin
2005-02-18q_*.cmo useless for making coqtopherbelin
2005-02-18Added bigint printerherbelin
2005-02-17majcoq
2005-02-17majcoq
2005-02-17Test bug #922herbelin
2005-02-17Correction bug #922 (problème dans depend) + formattage débogueurherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 05:14:38 +0000