index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
merge.ml
Age
Commit message (
Expand
)
Author
2018-01-24
Remove dead code from funind.
Maxime Dénès
2017-12-23
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-17
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-01
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-05-29
Cleanup: removal of constr_of_global.
Matthieu Sozeau
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-25
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-04
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-03-24
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-02-14
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Termops API using EConstr.
Pierre-Marie Pédrot
2016-10-19
CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".
Matej Kosik
2016-09-08
Merge PR #244.
Pierre-Marie Pédrot
2016-08-30
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-29
CLEANUP: taking advantage of "_ % _" operator to express function composition...
Matej Kosik
2016-08-24
CLEANUP: minor readability improvements
Matej Kosik
2016-08-19
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-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-18
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-16
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-10-28
Univs: local names handling.
Matthieu Sozeau
2015-10-13
Fix some typos.
Guillaume Melquiond
2015-09-14
Univs: Add universe binding lists to definitions
Matthieu Sozeau
[next]
