aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.mli
AgeCommit message (Expand)Author
2020-12-14Store the metasubst cache in clenvs.Pierre-Marie Pédrot
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-09-07Remove dead code in clenv-generating functions.Pierre-Marie Pédrot
2020-09-04Remove a unused function from the Clenv API.Pierre-Marie Pédrot
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
2020-06-24Actually remove internal API from the Clenv mli.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-05-12Remove a unused legacy tactic from Clenv.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-06Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)Gaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18Inlining the only use of Clenv.connect_clenv.Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-21Lazily check that an argument is dependent when constructing evar clauses.Pierre-Marie Pédrot
2014-10-21Adding an evar version of the make_clenv function.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-09-25Removing useless evar-related stuff.ppedrot
2013-06-04Backtrack on unneeded change of interface for pose_metas_as_evars.msozeau
2013-06-04Start documenting new [rewrite_strat] tactic that applies rewritingmsozeau
2013-04-29Merging Context and Sign.ppedrot
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-10Moved allow_K to a unification flagherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:41:49 +0000