index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
*
Merge PR #1114: Generic handling of nameable objects for plugins
Maxime Dénès
2017-10-09
|
\
*
|
[stm] [flags] Move document mode flags to the STM.
Emilio Jesus Gallego Arias
2017-10-06
|
*
Moving the Ltac-specific part of the nametab to the Ltac plugin.
Pierre-Marie Pédrot
2017-10-03
*
|
Removing now useless former fix to #3333 (check valid module names).
Hugo Herbelin
2017-09-12
|
/
*
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-31
|
\
*
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
|
|
*
Canonically renaming fold_map into fold_left_map in library Name.
Hugo Herbelin
2017-08-29
|
|
/
|
/
|
*
|
Print names of all open blocks
Tej Chajed
2017-08-06
|
*
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
|
/
*
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
|
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
|
Removing template polymorphism for definitions.
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
|
/
*
Merge PR #899: [general] Move files to directories so they match linking order.
Maxime Dénès
2017-07-20
|
\
*
|
Documenting the purity / marshallability invariant of persistent states.
Pierre-Marie Pédrot
2017-07-20
|
*
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
2017-07-19
|
/
*
Document the changes in API brought by this series of patches.
Pierre-Marie Pédrot
2017-07-14
*
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for Global.type_of_global_in_context.
Pierre-Marie Pédrot
2017-07-13
*
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
*
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
*
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
Merge PR #853: Clean 'with Definition' implementation.
Maxime Dénès
2017-07-06
|
\
*
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
Removing a few suspicious functions from the kernel.
Pierre-Marie Pédrot
2017-07-03
|
/
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Move univops from kernel to library
Amin Timany
2017-06-16
*
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
*
Fix bugs
Amin Timany
2017-06-16
*
Change the place of inference after sect discharge
Amin Timany
2017-06-16
*
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
*
Extend definition of inductives to include subtyping info
Amin Timany
2017-06-16
*
[lib] Remove obsolete state-management function add_frozen_state
Emilio Jesus Gallego Arias
2017-06-12
*
Use Names.Constant.print
Jason Gross
2017-06-02
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Don't double up on periods in anomalies
Jason Gross
2017-06-02
*
Remove a post merge warning.
Maxime Dénès
2017-06-01
*
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
*
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-29
|
\
|
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-27
|
/
*
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-25
|
\
*
\
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
\
*
\
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
\
|
|
*
|
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
/
|
|
*
Merge branch 'master' into ltac2-hooks
Pierre-Marie Pédrot
2017-05-19
|
|
|
\
|
|
|
/
|
|
/
|
[next]