index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
*
Notations: Do not consider a non-occurring variable as a binder-only variable.
Hugo Herbelin
2018-02-20
*
More precise explanation when a notation is not reversible for printing.
Hugo Herbelin
2018-02-20
*
Adding support for re-folding notation referring to isolated "forall '(x,y), t".
Hugo Herbelin
2018-02-20
*
Again one more step in fixing #5762 ("where" clause).
Hugo Herbelin
2018-02-20
*
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
*
Merge PR #1047: Support universe instances on the literal Type
Maxime Dénès
2018-02-12
|
\
*
\
Merge PR #6128: Simplification: cumulativity information is variance informa...
Maxime Dénès
2018-02-12
|
\
\
|
*
|
Use specialized function for inductive subtyping inference.
Gaëtan Gilbert
2018-02-11
|
*
|
Inference of inductive subtyping does not need an evar map.
Gaëtan Gilbert
2018-02-10
|
*
|
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
*
|
|
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
|
/
/
|
*
Support universe instances on the literal Type
Tej Chajed
2018-01-26
|
/
*
Merge PR #6532: Fix mli-doc issue #6531
Maxime Dénès
2018-01-08
|
\
|
*
Fix mli-doc issue #6531
Tony Beta Lambda
2018-01-01
*
|
Using a dedicated type for Lib.abstr_info.
Pierre-Marie Pédrot
2017-12-30
|
/
*
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Maxime Dénès
2017-12-27
|
\
*
\
Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...
Maxime Dénès
2017-12-27
|
\
\
|
|
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
|
|
/
|
/
|
*
|
Merge PR #6469: No universe constraints in Let definitions
Maxime Dénès
2017-12-22
|
\
\
*
\
\
Merge PR #6449: Let definitions must not contain side-effects when reaching t...
Maxime Dénès
2017-12-20
|
\
\
\
|
|
*
|
Let definitions do not create new universe constraints.
Pierre-Marie Pédrot
2017-12-19
|
|
*
|
Specific type for section definition entries.
Pierre-Marie Pédrot
2017-12-19
|
|
/
/
*
|
|
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
Maxime Dénès
2017-12-18
|
\
\
\
|
|
*
|
Let definitions must not contain side-effects when reaching the kernel.
Pierre-Marie Pédrot
2017-12-16
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`
Maxime Dénès
2017-12-15
|
\
\
\
|
|
*
|
[econstr] Switch constrintern API to non-imperative style.
Emilio Jesus Gallego Arias
2017-12-15
|
|
/
/
*
|
|
Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...
Maxime Dénès
2017-12-14
|
\
\
\
|
|
*
|
[econstr] Cleanup in `vernac/classes.ml`.
Emilio Jesus Gallego Arias
2017-12-13
|
|
/
/
|
/
|
|
|
*
|
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-12-12
|
*
|
Removing cumbersome location in multiple patterns.
Hugo Herbelin
2017-12-12
*
|
|
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
|
/
/
*
|
Merge PR #873: New strategy based on open scopes for deciding which notation ...
Maxime Dénès
2017-12-07
|
\
\
*
|
|
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-12-01
*
|
|
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
|
|
*
Remove unused boolean from cl_context field of Typeclasses.typeclass
Gaëtan Gilbert
2017-11-30
*
|
|
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-29
|
|
/
|
/
|
|
*
Selecting which notation to print based on current stack of scope.
Hugo Herbelin
2017-11-27
*
|
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
*
|
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
|
Stop exposing UState.universe_context and its Evd wrapper.
Gaëtan Gilbert
2017-11-24
*
|
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-24
*
|
Use type Universes.universe_binders.
Gaëtan Gilbert
2017-11-24
|
/
*
Merge PR #486: Make some functions on terms more robust w.r.t new term constr...
Maxime Dénès
2017-11-24
|
\
|
*
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
*
|
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
|
/
*
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-21
*
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Maxime Dénès
2017-11-21
|
\
*
\
Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.
Maxime Dénès
2017-11-20
|
\
\
*
\
\
Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...
Maxime Dénès
2017-11-20
|
\
\
\
[next]