aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/instances.ml
AgeCommit message (Expand)Author
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers from TacticalsPierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-03-03Fix bug #3732: firstorder was using detyping to build existentialMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:44:36 +0000