aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/sequent.ml
AgeCommit message (Expand)Author
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.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-08-01Detyping functions are now operating on EConstr.t.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-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
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-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach 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-01-20Update copyright headers.Maxime Dénès
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
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
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-18Fix bug #2227msozeau
2011-07-29Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Termpuech
2011-07-29Sequent: generic equality on global_reference replaced by RefOrdered.comparepuech
2011-07-29Sequent: generic equality on kernel_name replaced by kn_ordpuech
2011-07-29Sequent: generic equality on constr replaced by destructorspuech
2011-07-29Sequent: generic equality on ident replaced by id_ordpuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:48:10 +0000