aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-06-25Moved error when option does not exist into a warning (this allows toherbelin
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
2010-06-25modifs de nsatz suggerees par Hugopottier
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-23Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...notin
2010-06-23Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...notin
2010-06-22Commit 13179 continued (updated CHANGES about support for Heq's library).herbelin
2010-06-22Backport from trunk to 8.3 of modifications on groebner/nsatzherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-22Fixing dependencies for coqidevgross
2010-06-22fix bug #2318, parsing error on dos line endingsvgross
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix #2158...letouzey
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
2010-06-18clear/revert dependent: restrict to hyp(h) instead of ident(h)letouzey
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-18Documentation of clear dependent and revert dependentletouzey
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
2010-06-18Report fixes from FSetDecide to MSetDecideletouzey
2010-06-18fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...letouzey
2010-06-17fsetdec: clear dependent hypothesis before anything else (fix #2136).letouzey
2010-06-17New tactic "clear dependent", for the moment in ltac in Init/Tacticsletouzey
2010-06-16test for bug #2141 (include + extraction)letouzey
2010-06-16MSetInterface: no induction principle about a Record (nicer extraction)letouzey
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
2010-06-15MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...letouzey
2010-06-15CHANGE: a word about new commands Compute and Failletouzey
2010-06-15CHANGES: list of modifications for the extractionletouzey
2010-06-15Extraction: in support library, more and nicer big_intletouzey
2010-06-14Update of Extraction documentationletouzey
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-14Alert on the possible incompatibilties with set_add (see bug 2111) whichherbelin
2010-06-14Extraction Implicit: documentationletouzey
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
2010-06-13Fixing definition of set_map (bug report #2111) which was actually alreadyherbelin
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-13Made intros_until and onInductionArg a bit stricter and robustherbelin
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
2010-06-12Applying François' patch fixing grammar of uniform inheritance condition mes...herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 21:08:56 +0000