index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
merge.ml
Commit message (
Expand
)
Author
Age
*
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
*
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
*
CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".
Matej Kosik
2016-10-19
*
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
*
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
CLEANUP: taking advantage of "_ % _" operator to express function composition...
Matej Kosik
2016-08-29
*
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
/
/
*
|
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
|
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
|
*
Add corresponding field in `VernacInductive`.
Arnaud Spiwack
2015-06-24
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 15)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
More cleaning in CArray...
ppedrot
2012-09-18
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
[next]