aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/assumptions.ml
Commit message (Expand)AuthorAge
* FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
* Properly compute types for assumed section variables (bug #5035).Gravatar Guillaume Melquiond2016-08-24
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
* 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