aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Expand)AuthorAge
* Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
* Fix bug #5023: JSON extraction doesn't generate "for xxx".Gravatar Pierre-Marie Pédrot2016-10-17
* Extraction: ignore some useless stuff about universesGravatar Pierre Letouzey2016-09-29
* Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
| * Fix typo.Gravatar Guillaume Melquiond2016-06-23
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\|
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
* | 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
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 11:02:17 +0000