index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-10-17
Strings: add ByteVector
Yishuai Li
2018-10-17
Merge PR #8694: Various cleanups of universe apis
Pierre-Marie Pédrot
2018-10-17
Merge PR #8710: [omega, btauto] Remove some dead code
Pierre-Marie Pédrot
2018-10-17
Merge PR #8748: [dune] [plugins] Fix plugin name ground -> firstorder
Théo Zimmermann
2018-10-17
[dune] [plugins] Fix plugin name ground -> firstorder
Emilio Jesus Gallego Arias
2018-10-16
Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05
Pierre-Marie Pédrot
2018-10-16
Merge PR #8742: [clib] Remove Array functions available in OCaml 4.05.0
Pierre-Marie Pédrot
2018-10-16
Merge PR #8059: Simplify code for [Definition := Eval ...]
Matthieu Sozeau
2018-10-16
{Univops->UState}.restrict_universe_context
Gaëtan Gilbert
2018-10-16
{Univops -> Vars}.universes_of_constr
Gaëtan Gilbert
2018-10-16
UnivGen.extend_context -> Univ.extend_in_context_set
Gaëtan Gilbert
2018-10-16
Deprecate UnivGen.new_{univ,Type,Type_sort}
Gaëtan Gilbert
2018-10-16
Clean UnivGen.fresh_instance API
Gaëtan Gilbert
2018-10-16
Deprecate univ-dropping UnivGen.new_sort_in_family
Gaëtan Gilbert
2018-10-16
Simplify UnivGen.type_of_reference
Gaëtan Gilbert
2018-10-16
UnivGen.constr_of_glob_univ -> Constr.mkRef
Gaëtan Gilbert
2018-10-16
Remove [constr_of_global_in_context] in funind
Gaëtan Gilbert
2018-10-16
Simplify vars_of_global usage
Gaëtan Gilbert
2018-10-16
Simplify fresh_foo_instance functions and pretyping of univ instance
Gaëtan Gilbert
2018-10-16
Deprecate Global.universes_of_global (replaced by environ version)
Gaëtan Gilbert
2018-10-16
[Omega] Remove dead code
Vincent Laporte
2018-10-16
[btauto] Remove dead code
Vincent Laporte
2018-10-16
[omega] Remove dead code
Vincent Laporte
2018-10-16
Merge PR #8691: Remove some dead code in nsatz and micromega plugins
thery
2018-10-16
[clib] Remove Array functions available in OCaml 4.05.0
Emilio Jesus Gallego Arias
2018-10-16
[clib] Deprecate string functions available in OCaml 4.05
Emilio Jesus Gallego Arias
2018-10-16
[test-suite] Update csdp cache
Vincent Laporte
2018-10-16
[micromega] remove dead code
Vincent Laporte
2018-10-16
[nsatz] remove dead code
Vincent Laporte
2018-10-16
Merge PR #8695: Adding a functional version of constant- and mind_of_delta_kn...
Pierre-Marie Pédrot
2018-10-16
Merge PR #8733: Implement ARGUMENT EXTEND in coqpp
Emilio Jesus Gallego Arias
2018-10-15
Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.
Pierre-Marie Pédrot
2018-10-15
Port remaining EXTEND ml4 files to coqpp.
Pierre-Marie Pédrot
2018-10-15
Implement ARGUMENT EXTEND in coqpp.
Pierre-Marie Pédrot
2018-10-15
Plug ARGUMENT EXTEND into the argument extension API.
Pierre-Marie Pédrot
2018-10-15
Providing a centralized API for ARGUMENT EXTEND.
Pierre-Marie Pédrot
2018-10-15
Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.
Pierre-Marie Pédrot
2018-10-15
Merge PR #8689: A few useless accesses to the global environment in pretyping...
Pierre-Marie Pédrot
2018-10-15
Merge PR #8589: Correct some spelling errors (continued)
Emilio Jesus Gallego Arias
2018-10-15
Merge PR #8717: Lemmas, DeclareDef: internal reorganization of code highlight...
Emilio Jesus Gallego Arias
2018-10-15
Mini-factorization preparing unification.
Hugo Herbelin
2018-10-15
Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.
Hugo Herbelin
2018-10-15
DeclareDef: Reorganizing declaration of definitions in a more structured way.
Hugo Herbelin
2018-10-15
Merge PR #8716: Lemmas: Little simplification of artificially convoluted code
Emilio Jesus Gallego Arias
2018-10-15
Correct some spelling errors
Benjamin Barenblat
2018-10-15
Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.
Hugo Herbelin
2018-10-15
Merge PR #8732: [ci] [sf] Remove sed hacks from the SF build.
Gaëtan Gilbert
2018-10-14
[ci] [sf] Remove sed hacks from the SF build.
Emilio Jesus Gallego Arias
2018-10-14
A useless occurrence of Global.env.
Hugo Herbelin
2018-10-14
Parameterizing default inhabitant for impossible cases with an environment.
Hugo Herbelin
[next]