aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
Commit message (Expand)AuthorAge
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Fix unblocking code in dependent destruction due to zeta being used in unfold...Gravatar msozeau2012-02-01
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
* Making printing of backtick in Program reparsable (avoiding collision with "`(")Gravatar herbelin2011-06-14
* Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.Gravatar msozeau2011-06-07
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
* Add a flag to hide obligations in Program-generated terms under anGravatar msozeau2011-02-28
* In Program obligation, do not use auto on non-proposition goals byGravatar msozeau2011-02-17
* First release of Vector library.Gravatar pboutill2010-12-10
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Fix unfolding tactic for well-founded Programs.Gravatar msozeau2010-06-08
* Correction program_simplify. Devrait corriger certaines contribs.Gravatar aspiwack2010-05-28
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
* Minor fixes.Gravatar msozeau2010-03-05
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
* - Resolve type class constraints before trying to find unresolvedGravatar msozeau2009-09-11
* Misc fixes:Gravatar msozeau2009-09-10
* Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], asGravatar msozeau2009-09-03
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
* Use Type instead of Set.Gravatar msozeau2009-06-02
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Experimental support for automatic destruction of recursive calls andGravatar msozeau2009-04-08
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28