aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-05-02majcoq
2005-05-02Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...herbelin
2005-05-02Lemme de passage de l'autre côté d'une égalitéherbelin
2005-05-02Utilisation Z_scopeherbelin
2005-05-01majcoq
2005-04-30majcoq
2005-04-29majcoq
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug #...herbelin
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug #...herbelin
2005-04-29Improved order of interpretation of atomic tactics (cf bug #952)herbelin
2005-04-29Fix bug in prepare_predicate_from_tycon; improved error message when no claus...herbelin
2005-04-28majcoq
2005-04-27majcoq
2005-04-26majcoq
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
2005-04-25majcoq
2005-04-24majcoq
2005-04-23majcoq
2005-04-22majcoq
2005-04-21majcoq
2005-04-21majcoq
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
2005-04-20majcoq
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
2005-04-19majcoq
2005-04-18majcoq
2005-04-17majcoq
2005-04-16majcoq
2005-04-15majcoq
2005-04-14majcoq
2005-04-13majcoq
2005-04-12majcoq
2005-04-11majcoq
2005-04-10majcoq
2005-04-09majcoq
2005-04-08majcoq
2005-04-07majcoq
2005-04-07majcoq
2005-04-07dp: traitement des definitionscoq
2005-04-06majcoq
2005-04-05majcoq
2005-04-05Problemes de renommage reglescoq
2005-04-04majcoq
2005-04-03majcoq
2005-04-02majcoq
2005-04-01majcoq
2005-03-31majcoq
2005-03-31Added option_mapherbelin
2005-03-30majcoq
2005-03-29majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 04:18:00 +0000