aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2005-02-17Bug affichage entiers négatifsherbelin
2005-02-16majcoq
2005-02-15majcoq
2005-02-14majcoq
2005-02-13majcoq
2005-02-12majcoq
2005-02-12majcoq
2005-02-12Nouvelle mouture Print Canonical Structuresherbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
2005-02-12Uniformisation de destApplication en destApp; simplification decompose_appherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-11majcoq
2005-02-10majcoq
2005-02-10Ajout du reset des numéros d'états dans reset_initial. Plus proprecoq
2005-02-09majcoq
2005-02-08majcoq
2005-02-07majcoq
2005-02-07Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...coq