aboutsummaryrefslogtreecommitdiff
path: root/toplevel/obligations.ml
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-27Program: refine shrinking of obligationsMatthieu Sozeau
2016-06-27Rework treatment of default transparency of obligationsMatthieu Sozeau
2016-06-27Shrink Proofs/Obligations by default and deprecateMatthieu Sozeau
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.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-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-26Program: remove debug tracingMatthieu Sozeau
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-09Fix bug #3887: Better error message for "More than one program with unsolved ...Pierre-Marie Pédrot
2016-03-19Moving the use of Tactic_option from Obligations to G_obligations.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Univs/Program: update the universe context with global universeMatthieu Sozeau
2015-12-02Fix bug #4444: Next Obligation performed after a Section opening wasMatthieu Sozeau
2015-12-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-24Univs: carry on universe substitution when defining obligations ofMatthieu Sozeau
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Fix Next Obligation to not raise an anomaly in case of mutualMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:13:04 +0000