aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
Commit message (Expand)AuthorAge
* 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
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* - Better deal with commands inside section titles in latex output usingGravatar msozeau2009-01-21
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
* Fix for bug #1973 provided by Brian Campbell.Gravatar msozeau2008-10-22
* Suite 11472 et 11473Gravatar herbelin2008-10-19
* Various little improvements:Gravatar msozeau2008-09-25
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
* Remove redefinition of id in Program.Basics, just add maximal implicits.Gravatar msozeau2008-09-13
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Better handling of recursive Equations definitions... still not perfect.Gravatar msozeau2008-09-03
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* Various fixes:Gravatar msozeau2008-05-15
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20