aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.ml
Commit message (Expand)AuthorAge
* Preparing old-style refine from logic.ml to deal with "Cases" proofGravatar Hugo Herbelin2018-03-29
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
| * Exporting general-purpose functions on goal contexts from "logic.ml" to "tact...Gravatar Hugo Herbelin2017-06-25
|/
* Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\
* | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Fix call to broken unsafe_type_of in apply tactic.Gravatar Maxime Dénès2017-03-29
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping 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
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\
| * Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\| |
| * | Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
| | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| |/
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| |/ |/|
| * 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
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20