aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.ml
Commit message (Expand)AuthorAge
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Proof engine: support for nesting tactic-in-term within other tactics.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
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
| * 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
* Fix a refine anomaly "Evar defined twice".Gravatar Pierre-Marie Pédrot2017-09-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* Turn the default behaviour of the refine primitive into the safe one.Gravatar Pierre-Marie Pédrot2017-06-13
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
| * Generalizing the refine primitive so as to accept tactic arguments.Gravatar Pierre-Marie Pédrot2017-05-03
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
* | 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.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
| * Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
|/
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20