index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Extraction : add a location in the error message about polyprop
Pierre Letouzey
2016-05-30
*
Extraction/Projections: Fix bug #4710
Matthieu Sozeau
2016-05-23
*
Disable memoization rather than failing when files cannot be opened.
Guillaume Melquiond
2016-05-20
*
Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
Fix Haskell extraction for terms over 45 characters long
Nickolai Zeldovich
2016-05-04
*
Handle primitive projections inside types when extracting (bug #4616).
Guillaume Melquiond
2016-05-04
*
Remove extraneous space in coqtop/pg output (bug #4675).
Guillaume Melquiond
2016-05-03
*
Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
Nickolai Zeldovich
2016-04-09
*
Fixing a source of inefficiency and an artificial dependency in the
Daniel de Rauglaudre
2016-04-08
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
Extraction: msg_notice instead of msg_info.
Pierre Courtieu
2016-01-04
*
Inclusion of functors with restricted signature is now forbidden (fix #3746)
Pierre Letouzey
2015-12-22
*
Extraction: slightly better heuristic for Obj.magic simplifications
Pierre Letouzey
2015-12-16
*
Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications
Pierre Letouzey
2015-12-16
*
Extraction: more cautious use of intermediate result caching (fix #3923)
Pierre Letouzey
2015-12-15
*
Extraction: fix a few little glitches with my last commit (replacing unused v...
Pierre Letouzey
2015-12-15
*
Extraction: replace unused variable names by _ in funs and matchs (fix #2842)
Pierre Letouzey
2015-12-15
*
Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)
Pierre Letouzey
2015-12-14
*
Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)
Pierre Letouzey
2015-12-14
*
Extraction: cosmetically avoid generating spaces on empty lines
Pierre Letouzey
2015-12-14
*
Extraction: also get rid of explicit '\n' for haskell
Pierre Letouzey
2015-12-14
*
Extraction: fix a pretty-print issue
Pierre Letouzey
2015-12-14
*
Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")
Pierre Letouzey
2015-12-14
*
Extraction: nicer implementation of Implicits
Pierre Letouzey
2015-12-12
*
Extraction: check for remaining implicits after dead code removal (fix #4243)
Pierre Letouzey
2015-12-12
*
Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)
Pierre Letouzey
2015-12-12
*
Extraction: avoid generating some blanks at end-of-line
Pierre Letouzey
2015-12-12
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
*
Fix a bug preventing the generation of graphs when doing multiple
Matthieu Sozeau
2015-11-18
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Matthieu Sozeau
2015-10-28
*
Do not pause globing in funind. (Fix bug #4382)
Guillaume Melquiond
2015-10-28
*
Partly fixes #3225. Removed some old experimental stuff in funind.
Pierre Courtieu
2015-10-19
*
Exporting the original unprocessed hint in the hint running function.
Pierre-Marie Pédrot
2015-10-14
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
f_equal fix continued: do a refresh_universes as before.
Matthieu Sozeau
2015-10-08
*
Fix bug #4069: f_equal regression.
Matthieu Sozeau
2015-10-07
*
Univs: fix after rebase (from_ctx/from_env)
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map initialization in newring.
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map leaks bugs in Function
Matthieu Sozeau
2015-10-02
*
Univs: fix an evar leak in congruence
Matthieu Sozeau
2015-10-02
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Improve directives for Haskell extraction of nat.
Maxime Dénès
2015-09-03
*
Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v
Nickolai Zeldovich
2015-09-03
[next]