index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
library
Age
Commit message (
Expand
)
Author
2021-02-24
Infrastructure for fine-grained debug flags
Maxime Dénès
2021-01-22
Properly implement local references in Summary.
Pierre-Marie Pédrot
2020-12-02
Stop calling Id.Map.domain on univ binders every individual universe
Gaëtan Gilbert
2020-11-26
[kernel] Allow to set typing flags in add_mind [inductive]
Emilio Jesus Gallego Arias
2020-11-26
[kernel] Allow to set typing flags in add_constant
Emilio Jesus Gallego Arias
2020-11-25
Separate interning and pretyping of universes
Gaëtan Gilbert
2020-11-09
Remove the native symbol registering from the safe environment.
Pierre-Marie Pédrot
2020-10-21
Similar introduction of a Construct module in the Names API.
Pierre-Marie Pédrot
2020-10-21
Introduce an Ind module in the Names API.
Pierre-Marie Pédrot
2020-10-21
Rename the GlobRef comparison modules following the standard pattern.
Pierre-Marie Pédrot
2020-08-21
Use a map function instead of a fold when freezing summaries.
Pierre-Marie Pédrot
2020-06-30
[states] Move States to vernac
Emilio Jesus Gallego Arias
2020-05-15
[misc] Better preserve backtraces in several modules
Emilio Jesus Gallego Arias
2020-05-13
Make explicit that UGraph lower bounds are only of two kinds.
Pierre-Marie Pédrot
2020-04-28
Merge PR #12003: Improve error messages for Set and Unset commands.
Emilio Jesus Gallego Arias
2020-04-23
Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...
Pierre-Marie Pédrot
2020-04-20
Move new iter_table function to Goptions.
Théo Zimmermann
2020-04-20
Improve undeclared key messages.
Théo Zimmermann
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-04-13
correctly open objects for Names filters
Gaëtan Gilbert
2020-04-13
pass filters around
Gaëtan Gilbert
2020-04-13
Add ExtRefMap/Set to globnames
Gaëtan Gilbert
2020-04-06
Clean and fix definitions of options.
Théo Zimmermann
2020-04-03
Improve error messages for Set and Unset commands.
Théo Zimmermann
2020-03-30
Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creation
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-13
[cleanup] Remove unnecessary Map/Set module creation
Emilio Jesus Gallego Arias
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-02-13
Merge PR #11521: Remove Goptions.opt_name field
Pierre-Marie Pédrot
2020-02-12
Remove Goptions.opt_name field
Gaëtan Gilbert
2020-02-12
Standardize constr -> globref operations to use destRef/isRef/isRefX
Gaëtan Gilbert
2020-02-09
Remove the Template Check option.
Pierre-Marie Pédrot
2020-01-30
export_private_constants doesn't use the [constr in_univ_ctx] argument
Gaëtan Gilbert
2020-01-30
Merge PR #11307: Remove the hacks relying on hardwired libobject tags.
Maxime Dénès
2020-01-28
Remove dead code in Globnames.
Pierre-Marie Pédrot
2020-01-27
cleanup: Lib.freeze doesn't use its [~marshallable] argument
Gaëtan Gilbert
2019-12-22
Remove the hacks relying on hardwired libobject tags.
Pierre-Marie Pédrot
2019-12-22
Export the dynamic type API of libobjects.
Pierre-Marie Pédrot
2019-12-18
Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...
Pierre-Marie Pédrot
2019-12-13
Use ~strict argument consistently in push_context/push_context_set intfs
Matthieu Sozeau
2019-12-12
Merge PR #11278: Clean libobject stuff
Gaëtan Gilbert
2019-12-11
Remove the unused add_leaves Libobject primitive.
Pierre-Marie Pédrot
2019-12-09
Type-safe implementation of libobjects.
Pierre-Marie Pédrot
2019-12-09
Simplify the implementation of Summary by specifying the type of ML-MODULES.
Pierre-Marie Pédrot
2019-12-09
Type-safe implementation of summary state.
Pierre-Marie Pédrot
2019-12-07
Section.t is never empty
Gaëtan Gilbert
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-11-01
Declare type of primitives in CPrimitives
Pierre Roux
2019-10-24
[library] [nit] Remove unnecessary type alias.
Emilio Jesus Gallego Arias
2019-10-16
Split the function used to declare side-effects from the standard one.
Pierre-Marie Pédrot
[next]