aboutsummaryrefslogtreecommitdiff
path: root/toplevel/assumptions.ml
AgeCommit message (Expand)Author
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Print the type-in-type flag in various user-facing functions.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-04-04Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-09Print Assumptions: improve detection of case on an axiom of FalseEnrico Tassi
2015-09-20Fix #3948 Anomaly: unknown constant in Print AssumptionsMaxime Dénès
2015-09-15Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.Pierre-Marie Pédrot
2015-07-27Traversal of inductive defs in Print Assumptionsmlasson
2015-07-02Fix loop in assumptions (Close: #4275)Enrico Tassi
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:52:26 +0000