aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fixed wrong spelling in a warning.Gravatar herbelin2010-06-08
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Typo in ExtrOcamlString: list char instead of char listGravatar letouzey2010-06-08
* Fix unfolding tactic for well-founded Programs.Gravatar msozeau2010-06-08
* Tentative fix for typeclass resolution raising Evd.define exceptions.Gravatar msozeau2010-06-08
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Fix commentGravatar glondu2010-06-07
* Document grammar.cma->unix.cma dependency in CHANGESGravatar glondu2010-06-07
* Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)Gravatar glondu2010-06-07
* fixing error message display.Gravatar vgross2010-06-07
* Backporting part of r12970 to trunk (deprecation of double induction).Gravatar herbelin2010-06-07
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Updated performance analysis fileGravatar herbelin2010-06-06
* Extraction: attempt to provide nice extraction of chars and strings for OcamlGravatar letouzey2010-06-04
* Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-...Gravatar letouzey2010-06-04
* Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intGravatar letouzey2010-06-04
* doc Nstaz updatedGravatar pottier2010-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 13:40:12 +0000