index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
assumptions.ml
Age
Commit message (
Expand
)
Author
2021-01-04
Change the representation of kernel case.
Pierre-Marie Pédrot
2020-12-02
Move *_with_full_binders variants out of the kernel.
Pierre-Marie Pédrot
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-14
Use thunks to univ instead of lazy constr for template typing
Gaëtan Gilbert
2020-02-12
Check instance length in type_of_{inductive,constructor}
Gaëtan Gilbert
2020-02-09
Remove the Template Check option.
Pierre-Marie Pédrot
2019-10-24
Raise an anomaly when looking up unknown constant/inductive
Gaëtan Gilbert
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2019-08-16
Fix Print Assumptions: Inductive types can have unsafe fixpoints or
SimonBoulier
2019-08-16
Improve [Print Assumptions] for type-in-type and assumed positive.
SimonBoulier
2019-08-16
Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...
SimonBoulier
2019-07-08
[api] Deprecate GlobRef constructors.
Emilio Jesus Gallego Arias
2019-06-17
Merge PR #10362: Kernel-side delaying of polymorphic opaque constants
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
Allow to delay polymorphic opaque constants.
Pierre-Marie Pédrot
2019-05-24
Remove the indirect opaque accessor hooks from Opaqueproof.
Pierre-Marie Pédrot
2019-03-14
Repair relevance marks in-kernel.
Gaëtan Gilbert
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Proper record type and accessors for transparent states.
Pierre-Marie Pédrot
2018-10-12
Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.
Hugo Herbelin
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-09-25
Fixing #8532 (regression in Print Assumptions within a functor).
Hugo Herbelin
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
2018-09-05
Fixing #8416 (Print Assumptions missing module information from compiled files).
Hugo Herbelin
2018-04-07
Fixes #7192 (Print Assumptions does not enter implementation of submodules).
Hugo Herbelin
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-13
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-05-17
Merge branch 'v8.6'
Pierre-Marie Pédrot
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
