aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
Commit message (Expand)AuthorAge
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* COMMENT: Proofview.entryGravatar Matej Kosik2016-10-26
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Oops, my bad, didn't expect a merge issue!Gravatar Matthieu Sozeau2016-10-21
| * Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
| * Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Fixing #4906 (regression in printing an error message).Gravatar Hugo Herbelin2016-07-08
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
* Fix usage of Pervasives in goal selectors.Gravatar Cyprien Mangin2016-06-14
* Add a comment about the use of a zipper, for clarity.Gravatar Cyprien Mangin2016-06-14
* Add a [CList.partitioni] function.Gravatar Cyprien Mangin2016-06-14
* Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20