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-09-10
Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.
Hugo Herbelin
2018-09-10
Adding a command "Declare Scope" and deprecating scope implicit declaration.
Hugo Herbelin
2018-09-10
Merge PR #8104: Warnings on coercions used without being Imported
Enrico Tassi
2018-09-10
Bump version number to 8.10+alpha.
Guillaume Melquiond
2018-09-10
[dune] Add apidoc target using `odoc`
Emilio Jesus Gallego Arias
2018-09-10
[ci] [docker] Add more dependencies for Dune-aware jobs.
Emilio Jesus Gallego Arias
2018-09-10
Ltac2 overlay.
Hugo Herbelin
2018-09-10
Relying on the precomputation of the renaming also for new_evar_type.
Hugo Herbelin
2018-09-10
Fixing ltac names interpretation in internals of pattern-matching compilation.
Hugo Herbelin
2018-09-10
Fixing an inconsistency in interpreting Ltac names linking to binder names.
Hugo Herbelin
2018-09-10
Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.
Hugo Herbelin
2018-09-10
Temptative clarification of the role of ltac_genargs field in ltac_var_map.
Hugo Herbelin
2018-09-10
Minor cosmetic unifying of layout in pretyping.ml.
Hugo Herbelin
2018-09-10
Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments.
Hugo Herbelin
2018-09-10
Deprecate romega in favor of lia.
Vincent Laporte
2018-09-07
Bvector: add BVeq and some notations
Yishuai Li
2018-09-07
NArith: deprecate N2Bv_gen
Yishuai Li
2018-09-07
Merge PR #8437: Recover lost snippet
Théo Zimmermann
2018-09-07
Merge PR #8435: [dune] Fix build of coq_dune in 4.02.3
Théo Zimmermann
2018-09-07
Recover lost snippet
Matěj G
2018-09-07
Merge PR #8428: Add utop to default.nix for use in nix-shell (see #8426).
Vincent Laporte
2018-09-07
[dune] Fix build of coq_dune in 4.02.3
Emilio Jesus Gallego Arias
2018-09-07
Fix bug #8432 : program fixpoint and universes
Matthieu Sozeau
2018-09-07
Warnings on coercions used without being Imported
Maxime Dénès
2018-09-07
Merge PR #8423: coqpp: allow DEPRECATED when declaring tactics
Pierre-Marie Pédrot
2018-09-07
Canonical representation of kernel substitutions.
Pierre-Marie Pédrot
2018-09-07
Remove dead code in Mod_subst.
Pierre-Marie Pédrot
2018-09-07
Move to a team of code owners for the Nix files.
Théo Zimmermann
2018-09-07
Add utop to default.nix for use in nix-shell (see #8426).
Théo Zimmermann
2018-09-07
Merge PR #8426: [dune] [doc] Document `dune utop $lib`
Théo Zimmermann
2018-09-07
Merge PR #8411: Changes to default.nix to be able to use Dune.
Vincent Laporte
2018-09-06
Merge PR #8412: [dune] [ci] Fix and test release profile + use 1.1 dune-works...
Gaëtan Gilbert
2018-09-06
[dune] [doc] Document `dune utop $lib`
Emilio Jesus Gallego Arias
2018-09-06
[dune] [ci] Fix and test release profile + use 1.1 dune-workspace
Emilio Jesus Gallego Arias
2018-09-06
Deprecation warning in legacy tacextend.mlp
Vincent Laporte
2018-09-06
deprecation is CODE instead of IDENT
Vincent Laporte
2018-09-06
Bound proof-search in default program obligation tactic.
Matthieu Sozeau
2018-09-06
Fixing #8270 (cbn was calling zeta even when not asked for).
Hugo Herbelin
2018-09-06
coqpp: allow DEPRECATED when declaring tactics
Vincent Laporte
2018-09-06
Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.
Pierre-Marie Pédrot
2018-09-06
Merge PR #8394: Print the entire string to the CoqIDE screen, e.g. for "Print...
Pierre-Marie Pédrot
2018-09-06
Merge PR #8415: [bin] Fix binary location procedure to work with symlinks.
Pierre-Marie Pédrot
2018-09-06
Merge PR #8420: [pfedit] Fix master build due to merge conflict
Gaëtan Gilbert
2018-09-06
[pfedit] Fix master build due to merge conflict
Emilio Jesus Gallego Arias
2018-09-06
Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with Program
Matthieu Sozeau
2018-09-06
Override Dune derivation to update it before nixpkgs.
Théo Zimmermann
2018-09-06
Changes to default.nix to be able to use Dune.
Théo Zimmermann
2018-09-06
Merge PR #8295: Fix #8291: print universe names in universe context for Check.
Matthieu Sozeau
2018-09-05
Fixing #8416 (Print Assumptions missing module information from compiled files).
Hugo Herbelin
2018-09-05
[bin] Fix binary location procedure to work with symlinks.
Emilio Jesus Gallego Arias
[prev]
[next]