aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Expand)AuthorAge
* Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
* Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * 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
* | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Gravatar Pierre Letouzey2016-05-04
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\ \ \ | | |/ | |/|
* | | Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
| * | Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | * Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-02-19
| |/ |/|
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \ \ | | |/ | |/|
| * | Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\| |
| * | Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\| |
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| |/ |/|
| * 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 some typos.Gravatar Guillaume Melquiond2015-10-13
* 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
* Fixing bug #4186.Gravatar Pierre-Marie Pédrot2015-04-13
* JSON extraction: make explicit each group of mutually-recursive fixpointsGravatar Nickolai Zeldovich2015-04-09
* JSON extraction: construct full names (dot-separated) in pp_globalGravatar Nickolai Zeldovich2015-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 08:45:03 +0000