aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Export Proofview.undefined as "unsafe" primitive.Gravatar Hugo Herbelin2018-03-27
* Adding informative variant of shelve_unifiable returning set of shelved evars.Gravatar Hugo Herbelin2018-03-27
* A comment in Proofview.with_shelf.Gravatar Hugo Herbelin2018-03-08
* Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Gravatar Hugo Herbelin2018-03-08
* Proof engine: using save_future_goal when relevant.Gravatar Hugo Herbelin2018-03-08
* Proof engine: consider the pair principal and future goals as an entity.Gravatar Hugo Herbelin2018-03-08
* Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Proofview: V82.tactic option to not normalize evarsGravatar Enrico Tassi2018-03-04
* | proofview: debug API to print a goalGravatar Enrico Tassi2018-03-04
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* | proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
* Proofview: enter_one: add __LOC__ argument to get relevant error msgGravatar Enrico Tassi2018-01-31
* Merge PR #6222: Share computation of unifiable evarsGravatar Maxime Dénès2017-12-22
|\
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| * Experimenting with a fine-grained cache for undefined evars in evinfos.Gravatar Pierre-Marie Pédrot2017-11-21
| * Fix #6204: `refine` is exponential in the number of fresh evars that it creates.Gravatar Pierre-Marie Pédrot2017-11-21
|/
* Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
* 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