index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
discharge.ml
Commit message (
Expand
)
Author
Age
*
[deps] Move `Discharge` to `interp`
Emilio Jesus Gallego Arias
2017-10-09
*
Discharge.ml: cosmetic renaming of some variables.
Hugo Herbelin
2017-09-23
*
Fixing #5755 (discharging of inductive types not correct with let-ins).
Hugo Herbelin
2017-09-23
*
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
*
Change the place of inference after sect discharge
Amin Timany
2017-06-16
*
Subtyping inference for inductoves and records
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
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
*
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
2017-02-15