aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.ml
AgeCommit message (Expand)Author
2016-09-16Adding variants enter_one and refine_one which assume that exactly oneHugo Herbelin
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-07-08Fixing #4906 (regression in printing an error message).Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-16Proofview: extensions for backtracking eautoMatthieu Sozeau
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Add a comment about the use of a zipper, for clarity.Cyprien Mangin
2016-06-14Add a [CList.partitioni] function.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:37:32 +0000