aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.mli
Commit message (Expand)AuthorAge
* [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
* Putting implicit arguments of Clenv.res_pf right.Gravatar Pierre-Marie Pédrot2014-06-25
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.unify is in the new monad.Gravatar Pierre-Marie Pédrot2014-06-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* simplification de clenvGravatar barras2004-09-10
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 19:29:57 +0000