index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
himsg.ml
Age
Commit message (
Expand
)
Author
2018-02-02
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2017-11-22
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-13
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-09-22
Himsg: Dropping nf_evars made obsolete by EConstr.
Hugo Herbelin
2017-09-22
Cannot unify message: improve preventing repeating twice the same message.
Hugo Herbelin
2017-09-15
Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.
Maxime Dénès
2017-09-12
Port is_Set and is_Type to EConstr, as was is_Prop already.
Guillaume Melquiond
2017-08-30
Fixing a capitalization in the middle of the sentence of an error message.
Hugo Herbelin
2017-08-01
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-07-26
Remove a few useless evar-normalizations in printing code.
Pierre-Marie Pédrot
2017-07-13
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-05-31
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
