summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-08Adding support for OCaml 4.06.0 (option -unsafe-string needed).refs/pull/6356/headv8.4Hugo Herbelin
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Hugo Herbelin
2017-05-04Adding an option "Set Debug Cbv" for printing visited constants during cbv.Hugo Herbelin
2017-04-27Protecting the '-time' flag from changes in the summary.Pierre-Marie Pédrot
2017-03-12Updating a misleading comment in Logic library.Hugo Herbelin
2017-02-25Fixing a little ennoying approximation in configure when detecting camlp5.Hugo Herbelin
2017-02-08Extraction: adapt the test-suite after 4b1429d (was a fix for #2842)Pierre Letouzey
2017-02-07Extraction: an extra space forgotten in previous commitPierre Letouzey
2017-02-04Extraction: fix complexity issue #5310Pierre Letouzey
2016-05-04Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-03-14Disable warning 31 when generating coqtop from coqmktop.Maxime Dénès
2016-02-16Warn when including functors with restricted signature (fix for #3746).Pierre Letouzey
2016-01-13v8.4: Fix for #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
2015-12-14Extraction: fix a pretty-print issuePierre Letouzey
2015-12-14Extraction: check for remaining implicits after dead code removal (fix #4243)Pierre Letouzey
2015-12-14Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Pierre Letouzey
2015-11-22v8.4: Fixing critical bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-16v8.4: Reverting "compare stacks head first!" which is breaking theHugo Herbelin
2015-11-07v8.4: Fixing documention of Add Printing Coercion.Hugo Herbelin
2015-10-26Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Pierre Letouzey
2015-10-24v8.4: Fixing a loop in checking hints with holes.Hugo Herbelin
2015-10-15compare stacks head first!Bruno Barras
2015-10-14minor update of checker/includeBruno Barras
2015-10-14fix problem with mixed mono/poly inductive definitionsBruno Barras
2015-10-14Remove dead code in lazy reduction machine.Maxime Dénès
2015-10-14improve efficiency of the reduction interpreter of coqtopBruno Barras
2015-10-14improve efficiency of the reduction interpreter of the checkerBruno Barras
2015-09-09Fix on backport of bugfix for depelim in 8.4.Matthieu Sozeau
2015-09-09Backport fix for bug 4294Matthieu Sozeau
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-07-28Fix for previous commit (debug function committed by mistake).Hugo Herbelin
2015-07-28v8.4: Fixing bug #4289 (hash-consing only user part of constant notHugo Herbelin
2015-07-16Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Hugo Herbelin
2015-06-23Puts all the "import" statements first so as to accommodate the latest GHC.Nickolai Zeldovich
2015-06-23Define Any in Haskell extraction when Tunknown is used.Nickolai Zeldovich
2015-06-23Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
2015-06-23Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-06-23Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Guillaume Melquiond
2015-06-23Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsNickolai Zeldovich
2015-06-23Haskell extraction: put unsafeCoerce type declaration laterNickolai Zeldovich
2015-06-22Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-04-21v8.4: Fixing #3376 and #4191 (wrong index of maximally-insertedHugo Herbelin
2015-04-09v8.4: restore compatibility with OCaml 3.11.2Pierre Letouzey
2015-04-09Changelog for 8.4pl6V8.4pl6Pierre Letouzey
generated by cgit v0.10.2-6-g49f6 at 2024-05-07 04:39:27 (GMT)