aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.ml
Commit message (Expand)AuthorAge
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
* | Code simplification in elim.ml.Gravatar Hugo Herbelin2016-01-20
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Define Tactics.bring_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-03-28
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Less use of the list-based interface for goal-bound tactics.Gravatar aspiwack2013-11-02
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Modulification of identifierGravatar ppedrot2012-12-14
* still some more dead code removalGravatar letouzey2012-10-06
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30