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: replace unused variable names by _ in funs and matchs (fix #2842)
Pierre Letouzey
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
*
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
|
Getting rid of dynamic hacks in Setoid_newring.
Pierre-Marie Pédrot
2015-12-04
*
|
Removing the last use of tacticIn in setoid_ring.
Pierre-Marie Pédrot
2015-12-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
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
*
|
Preventing an unwanted warning 5 "this function application is partial"
Hugo Herbelin
2015-11-07
*
|
Merge remote-tracking branch 'origin/v8.5' into upstream-trunk
Hugo Herbelin
2015-11-07
|
\
|
|
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
*
|
Monotonizing Tactics.change_arg.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
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
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
*
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
*
|
Function debug mode more formatted.
Pierre Courtieu
2015-10-19
|
*
Partly fixes #3225. Removed some old experimental stuff in funind.
Pierre Courtieu
2015-10-19
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
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
[prev]
[next]