aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.mli
AgeCommit message (Expand)Author
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-06-25Putting implicit arguments of Clenv.res_pf right.Pierre-Marie Pédrot
2014-06-24Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itPierre-Marie Pédrot
2014-06-24Clenvtac.res_pf is in the new tactic monad.Pierre-Marie Pédrot
2014-06-23Clenvtac.unify is in the new monad.Pierre-Marie Pédrot
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-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-04-29Merging Context and Sign.ppedrot
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-03-02Noise for nothingpboutill
2011-06-10Moved allow_K to a unification flagherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2008-12-14Fix looping class resolution bug discovered by B. Aydemir and use themsozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:21:06 +0000