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
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.
Maxime Dénès
2017-11-03
|
\
*
\
Merge PR #6047: A generic printer for ltac values
Maxime Dénès
2017-11-03
|
\
\
|
*
|
Do not identify a pre_ident as a string Ltac value.
Hugo Herbelin
2017-11-02
|
|
*
Fix FIXME: use OCaml 4.02 generative functors when available.
Gaëtan Gilbert
2017-11-01
*
|
|
Fixing #5401 (printing of patterns with bound anonymous variables).
Hugo Herbelin
2017-10-28
|
/
/
*
/
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
|
/
*
Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...
Maxime Dénès
2017-10-20
|
\
*
|
[deps] Move `Discharge` to `interp`
Emilio Jesus Gallego Arias
2017-10-09
|
*
Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).
Hugo Herbelin
2017-10-05
*
|
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
|
/
*
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-26
|
\
|
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
|
Reporting locations in error messages about notation formats.
Hugo Herbelin
2017-09-18
|
/
*
Merge PR #1037: Parse directly to Sorts.family when appropriate.
Maxime Dénès
2017-09-15
|
\
*
|
Adding a missing period in a notation warning.
Hugo Herbelin
2017-09-12
*
|
Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.
Hugo Herbelin
2017-09-12
*
|
Fixing a typo in printing notations with recursive binders.
Hugo Herbelin
2017-09-12
*
|
Fixing a bug of recursive notations introduced in dfdaf4de.
Hugo Herbelin
2017-09-12
*
|
Fixing little inaccuracy in coercions to ident or name.
Hugo Herbelin
2017-09-12
|
*
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-09-08
|
/
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-31
|
\
*
\
Merge PR #946: Functional pretyping interface
Maxime Dénès
2017-08-29
|
\
\
*
\
\
Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...
Maxime Dénès
2017-08-29
|
\
\
\
*
\
\
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
\
\
|
|
*
|
|
A new step of restructuration of notations.
Hugo Herbelin
2017-08-29
|
|
*
|
|
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-08-29
|
|
/
/
/
|
/
|
|
|
|
|
|
*
Adapting code to renaming Array.fold_map -> Array.fold_left_map.
Hugo Herbelin
2017-08-29
|
|
|
*
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
Hugo Herbelin
2017-08-29
|
|
_
|
/
|
/
|
|
|
*
|
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
|
|
*
Remove understand_tcc_evars.
Maxime Dénès
2017-08-01
|
|
/
*
/
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-08-01
|
/
*
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
*
\
Merge PR #889: Removing template polymorphism for definitions.
Maxime Dénès
2017-07-28
|
\
\
*
\
\
Merge PR #888: Stronger kernel types
Maxime Dénès
2017-07-28
|
\
\
\
|
|
|
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
|
|
*
|
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
|
|
/
/
*
|
|
Merge PR #894: Fixing a little location bug with recursive binders
Maxime Dénès
2017-07-26
|
\
\
\
|
|
_
|
/
|
/
|
|
|
|
*
Further simplication: do not recreate entries for side-effects.
Pierre-Marie Pédrot
2017-07-26
|
|
*
Remove a horrendous hack in Declare to retrieve exported side-effects.
Pierre-Marie Pédrot
2017-07-26
|
|
*
More precise type of entries capturing their lack of side-effects.
Pierre-Marie Pédrot
2017-07-26
|
|
*
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
|
|
/
|
/
|
*
|
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
2017-07-19
|
*
Fixing a little location bug with recursive binders.
Hugo Herbelin
2017-07-18
*
|
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
|
/
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
*
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
Merge PR#713: Bump year in headers.
Maxime Dénès
2017-06-15
|
|
\
*
|
\
Merge PR#719: Constrexpr.Numeral without bigint
Maxime Dénès
2017-06-15
|
\
\
\
[next]