aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
* Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
* Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
* Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* Extraction: also get rid of explicit '\n' for haskellGravatar Pierre Letouzey2015-12-14
* Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
* Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Gravatar Pierre Letouzey2015-12-14
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: check for remaining implicits after dead code removal (fix #4243)Gravatar Pierre Letouzey2015-12-12
* Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Gravatar Pierre Letouzey2015-12-12
* Extraction: avoid generating some blanks at end-of-lineGravatar Pierre Letouzey2015-12-12
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Fix a bug preventing the generation of graphs when doing multipleGravatar Matthieu Sozeau2015-11-18
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
* Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* f_equal fix continued: do a refresh_universes as before.Gravatar Matthieu Sozeau2015-10-08
* Fix bug #4069: f_equal regression.Gravatar Matthieu Sozeau2015-10-07
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* Univs: fix an evar leak in congruenceGravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Improve directives for Haskell extraction of nat.Gravatar Maxime Dénès2015-09-03
* Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vGravatar Nickolai Zeldovich2015-09-03
* Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vGravatar Nickolai Zeldovich2015-09-03
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Add efficient extraction of [nat], [Z], and [string] to HaskellGravatar Nickolai Zeldovich2015-06-22
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 08:32:22 +0000