summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-27Adding support for OCaml 4.06.0 (option -unsafe-string needed).refs/pull/6362/headv8.2Hugo Herbelin
2017-12-27Updating configure with ocaml >= 4.03.0.Hugo Herbelin
2017-12-27Not recommending 4.02.0.Hugo Herbelin
2017-12-27Fixing test for compilation under MacOS X pentium.Hugo Herbelin
2017-12-09A fix for compilation with OCaml 4.04.0.Hugo Herbelin
2017-12-09Fixing a little ennoying approximation in configure when detecting camlp5.Hugo Herbelin
2016-03-02Ensuring that sed does not use a specific locale for characters >= 128,Hugo Herbelin
2016-01-13v8.2: Fix for #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2015-12-02Being more robust on the location of lablgtk2 for coqmktop.ml.Hugo Herbelin
2015-12-02Updating INSTALL about 3.08.3.Hugo Herbelin
2015-11-29Backward OCaml compatibility (3.08).Hugo Herbelin
2015-11-29Updating CHANGES.Hugo Herbelin
2015-11-29Test for critical bug #4157.Hugo Herbelin
2015-11-26v8.2: Compatibility with compilation with Ocaml4Hugo Herbelin
2015-11-26v8.2: Backporting Arnaud's fix for compilation with Ocaml version 4.03.Arnaud Spiwack
2015-11-26v8.2: supporting compilation of coqide with lablgtk 2.16 and 2.18.Hugo Herbelin
2015-11-26Compatibility MacOS in hostname. Reported by Benjamin.Hugo Herbelin
2015-09-09Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-09Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-04-01Fix bug 4157 (vm compute on inductive with more than 245 constructors)Benjamin Gregoire
2015-01-29v8.2: backporting Pierre Boutillier's fix to #3843 part 2: "The .cmxsHugo Herbelin
2015-01-29v8.2: Applying Xavier Leroy's patch for cmxs installation on cygwin (#3843).Hugo Herbelin
2014-04-11Fix guard condition for nested cofixpoints in checker.Maxime Dénès
2014-04-11Fix guard condition for nested cofixpoints.Maxime Dénès
2014-03-05Fix (3243): univ constraints of module subtyping were not propagatedEnrico Tassi
2014-02-26Fix for critical bug in arity check.Maxime Dénès
2014-02-26configure stript allows make v4.00pboutill
2013-11-29v8.2: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notHugo Herbelin
2013-11-25v8.2: Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
2013-06-02v8.2: Fixing a typo in the documentation of discriminate.herbelin
2013-02-05Fixed #2839 and #2981 (anomaly NotASort in retyping). Was due toherbelin
2013-01-28v8.2: Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
2013-01-27v8.2: Fixed bug #2967 (missing check on ill-formed recursive notation strings).herbelin
2012-10-17v8.2: Removed mention of configure's option -nowarning in INSTALL file.herbelin
2012-09-05v8.2: A few fixes in configure file:herbelin
2012-08-03Bigint: adds a missing -1 in hugo's last commit 15659letouzey
2012-07-29v8.2: Better fixing propagation of carry in sub_mult used for euclidianherbelin
2012-07-25Compatibility with camlp5 6.05 (Closes: #2728)glondu
2012-07-25Fix compilation with camlp5 in strict mode (Closes: #2487)glondu
2012-07-21v8.2: Fixing unchecked overflow in sub_mult used for euclidian division overherbelin
2012-04-19v8.2: Supporting optional byte-mark order in utf-8 files (bug #2757).herbelin
2012-03-13v8.2: Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2011-12-19version bumpnotin
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-10-12Patch to support (a priori) all versions of make 3.xx >= 3.81herbelin
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-10-01Fixing critical part of bug #2504. Not all inductive types in Type areherbelin
2011-07-06Backporting critical bug fix r13450 from trunk/8.3 to branch 8.2.herbelin
2011-06-14Making printing of backtick in Program reparsable (avoiding collision with "`(")herbelin
generated by cgit v0.10.2-6-g49f6 at 2024-04-24 12:46:10 (GMT)