aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/assumptions.ml
Commit message (Expand)AuthorAge
* Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...Gravatar Matej Kosik2016-04-04
|\
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ /
* | Print Assumptions: improve detection of case on an axiom of FalseGravatar Enrico Tassi2015-12-09
* | Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
* | Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Gravatar Pierre-Marie Pédrot2015-09-15
| * Traversal of inductive defs in Print AssumptionsGravatar mlasson2015-07-27
|/
* Fix loop in assumptions (Close: #4275)Gravatar Enrico Tassi2015-07-02
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29