aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
Commit message (Expand)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...Gravatar Maxime Dénès2017-07-07
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * In enter_one, not having exactly one goal is a fatal error of the monad.Gravatar Hugo Herbelin2017-06-23
|/
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Fix an optimization failure in tclPROGRESS.Gravatar Pierre-Marie Pédrot2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* "tclENV" is sexier, use it instead of "Env.get"Gravatar Matej Kosik2017-04-20
* reduce syntactic noiseGravatar Matej Kosik2017-04-20
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | 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
| * Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
| * Merge remote-tracking branch 'github/pr/350' into trunkGravatar Maxime Dénès2017-01-09
| |\
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| |
| | * tclDISPATCH: more informative error messageGravatar Arnaud Spiwack2016-11-08
| |/ |/|
* | COMMENT: Proofview.entryGravatar Matej Kosik2016-10-26
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\ \
| | * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
| |/
| * 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