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-23
[dune] [opam] Move to OPAM 2.0
Emilio Jesus Gallego Arias
2018-10-23
Merge PR #8798: Order Greek letters consistently w/rest of document
Théo Zimmermann
2018-10-23
Merge PR #8799: Fix formatting. Use standard if..then grammar.
Théo Zimmermann
2018-10-23
Merge PR #8802: [dune] Install man pages + remove two obsolete ones.
Théo Zimmermann
2018-10-23
Merge PR #8786: Adding a regression test for bug #8785: universe constraints ...
Pierre-Marie Pédrot
2018-10-23
Merge PR #8797: [doc] [api] Update `odoc` to new release 1.3.0
Gaëtan Gilbert
2018-10-23
[dune] Install man pages + remove two obsolete ones.
Emilio Jesus Gallego Arias
2018-10-23
Fix formatting. Use standard if..then grammar.
Sam Pablo Kuper
2018-10-23
Order Greek letters consistently w/rest of document
Sam Pablo Kuper
2018-10-22
[doc] [api] Update `odoc` to new release 1.3.0
Emilio Jesus Gallego Arias
2018-10-22
Merge PR #8708: Stupid but critical unfolding heuristic.
Maxime Dénès
2018-10-22
Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.ml
Théo Zimmermann
2018-10-21
Adding a regression test for bug #8785 (missing univ constraints registration).
Hugo Herbelin
2018-10-20
Merge PR #8769: [library] Remove redundant re-addition of universe constraints.
Gaëtan Gilbert
2018-10-20
[dune] Remove rule for cLexer.ml4 -> cLexer.ml
Emilio Jesus Gallego Arias
2018-10-20
Merge PR #8782: gitignore test-suite/.nia.cache
Théo Zimmermann
2018-10-19
Merge PR #8758: [api] Qualify access to `Nametab`
Hugo Herbelin
2018-10-19
gitignore test-suite/.nia.cache
Gaëtan Gilbert
2018-10-19
Merge PR #8724: [universes] deprecate constr_of_global
Pierre-Marie Pédrot
2018-10-19
Merge PR #8740: Removing the Camlp5 macros from CLexer.
Emilio Jesus Gallego Arias
2018-10-18
[library] Remove redundant re-addition of universe constraints.
Emilio Jesus Gallego Arias
2018-10-18
Merge PR #8719: [ci] [appveyor] Disable validate target.
Maxime Dénès
2018-10-18
Merge PR #8670: Document the issue with positive coinductive types.
Théo Zimmermann
2018-10-18
Adding a rule to generate grammar.cma.
Pierre-Marie Pédrot
2018-10-18
Removing the Camlp5 macros from CLexer.
Pierre-Marie Pédrot
2018-10-18
[universes] deprecate constr_of_global
Matthieu Sozeau
2018-10-18
[api] Qualify access to `Nametab`
Emilio Jesus Gallego Arias
2018-10-18
Merge PR #8761: [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.
Emilio Jesus Gallego Arias
2018-10-18
[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.
Théo Zimmermann
2018-10-18
Merge PR #8756: [micromega] Build csdpcert
Vincent Laporte
2018-10-18
Merge PR #8754: [doc] [build] Remove ocamlbuild leftovers.
Théo Zimmermann
2018-10-17
[micromega] Build csdpcert
Emilio Jesus Gallego Arias
2018-10-17
[doc] [build] Remove ocamlbuild leftovers.
Emilio Jesus Gallego Arias
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
[next]