aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Report fixes from FSetDecide to MSetDecideGravatar letouzey2010-06-18
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...Gravatar letouzey2010-06-18
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
* New tactic "clear dependent", for the moment in ltac in Init/TacticsGravatar letouzey2010-06-17
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
* MSetInterface: no induction principle about a Record (nicer extraction)Gravatar letouzey2010-06-16
* Extraction: fix the eta reduction function used in code optimisationsGravatar letouzey2010-06-16
* MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...Gravatar letouzey2010-06-15
* CHANGE: a word about new commands Compute and FailGravatar letouzey2010-06-15
* CHANGES: list of modifications for the extractionGravatar letouzey2010-06-15
* Extraction: in support library, more and nicer big_intGravatar letouzey2010-06-15
* Update of Extraction documentationGravatar letouzey2010-06-14
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Alert on the possible incompatibilties with set_add (see bug 2111) whichGravatar herbelin2010-06-14
* Extraction Implicit: documentationGravatar letouzey2010-06-14
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
* Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withGravatar herbelin2010-06-13
* Fixing definition of set_map (bug report #2111) which was actually alreadyGravatar herbelin2010-06-13
* Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"Gravatar herbelin2010-06-13
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Made intros_until and onInductionArg a bit stricter and robustGravatar herbelin2010-06-13
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
* Applying François' patch fixing grammar of uniform inheritance condition mes...Gravatar herbelin2010-06-12
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Improved the inference of the return predicate in dependent pattern-matching.Gravatar herbelin2010-06-12
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
* Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).Gravatar herbelin2010-06-12
* Added debugging printer for the idmap used at evar definition time forGravatar herbelin2010-06-12
* Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.Gravatar herbelin2010-06-11
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Fixed two bugs in pattern-matching compilationGravatar herbelin2010-06-10
* Fixed a very old (from V6.3) typo in headers.styGravatar herbelin2010-06-10
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
* Fix build with OCaml 3.12Gravatar glondu2010-06-10
* Fixed bug # 2303 in r 13087.Gravatar msozeau2010-06-09
* Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in aGravatar msozeau2010-06-09
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Keep description of Automatic Introduction at only one place of CHANGES.Gravatar herbelin2010-06-09
* Relaxed the freshness constraint in "intro H" (with "H" explicit):Gravatar herbelin2010-06-09
* Allowing to use an ordering different than Lt with measureGravatar jforest2010-06-09
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).Gravatar herbelin2010-06-08
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 12:21:45 +0000