index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
elimschemes.ml
Age
Commit message (
Expand
)
Author
2020-04-28
Return an option in lookup_scheme.
Pierre-Marie Pédrot
2020-04-28
Stop relying on side-effects for recursive scheme declaration.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-01-27
schemes: use rigid universes
Gaëtan Gilbert
2019-12-10
Side-effect free wrapper around already declared schemes.
Pierre-Marie Pédrot
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-11
Remove the side-effect role from the kernel.
Pierre-Marie Pédrot
2019-06-07
Merge PR #10205: Make discriminate tactic compatible with HoTT
Pierre-Marie Pédrot
2019-06-06
Make discriminate tactic compatible with HoTT
Andreas Lynge
2019-05-23
Fixing typos - Part 3
JPR
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2018-07-03
Remove unused env argument to fresh_sort_in_family
Gaëtan Gilbert
2018-04-17
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
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-07-13
Getting rid of AUContext abstraction breakers in Elimschemes.
Pierre-Marie Pédrot
2017-07-11
Safe API for accessing universe constraints of global references.
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-06-16
Squashed commit of the following:
Amin Timany
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2016-07-29
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-29
Fix #4769, univ poly and elim schemes in sections
Matthieu Sozeau
2016-07-06
primproj: warning and avoid error.
Matthieu Sozeau
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-10-29
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-28
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-09-23
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-09-14
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-08-02
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-01-17
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-08-14
Fix elimschemes accessing directly the universe context of inductives (fixes ...
Matthieu Sozeau
2014-06-18
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-17
Removing dead code.
Pierre-Marie Pédrot
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2013-08-08
State Transaction Machine
gareuselesinge
2012-10-02
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-08-08
Updating headers.
herbelin
2011-05-26
Fixing discriminate for identity.
herbelin
2010-09-24
Some dead code removal, thanks to Oug analyzer
letouzey
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2009-12-13
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
