aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* clearing unused functionsGravatar vgross2009-06-22
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Try typeclass resolution in coercion if no solution can be found to aGravatar msozeau2009-06-18
* Fallback on not using [fix_proto] if the right imports aren't there, the Gravatar msozeau2009-06-17
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
* Correct typo: -noglob takes no argument.Gravatar msozeau2009-06-13
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar msozeau2009-06-11
* Accept more Unicode symbolsGravatar glondu2009-06-10
* Use the projections for reflexivity, symmetry and transitivity proofs toGravatar msozeau2009-06-10
* Correct handling of the initial existentials from the goal and the onesGravatar msozeau2009-06-09
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
* Change in UI behaviour : proof folding is now done by double clicking. Delay isGravatar vgross2009-06-08
* File forgotten in commit 12171.Gravatar herbelin2009-06-07
* Partial simplification of undo mechanism, relying only on Courtieu'sGravatar herbelin2009-06-07
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Makefile made compatible with Solaris 10 (bug #2078, continued - seeGravatar herbelin2009-06-06
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Very-small-step policy changes to the library.Gravatar herbelin2009-06-06
* Applying Ian Lynagh's documentation fixes patch (see bug #2112)Gravatar herbelin2009-06-06
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Use Type instead of Set.Gravatar msozeau2009-06-02
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2009-06-01
* Change unification with sort constraints to not use the kernelGravatar msozeau2009-06-01
* Prevent automatic inference of implicit arguments when the auto flag isGravatar msozeau2009-06-01
* Fix extract hyps to correctly discharge all hyps as described by keepGravatar msozeau2009-05-29
* Properly catch sort constraint inconsistency exception inGravatar msozeau2009-05-28
* Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.Gravatar courtieu2009-05-28
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Populate the sort constraints set correctly during unification. Add aGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansGravatar aspiwack2009-05-27
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...Gravatar aspiwack2009-05-27
* sane behaviour for copy/paste operations (the code is still insane, though)Gravatar vgross2009-05-27
* keeping interface synch'edGravatar vgross2009-05-27
* dead code pruningGravatar vgross2009-05-27
* Fix de Bruijn lifting bug appearing when we match on multiple terms withGravatar msozeau2009-05-26
* ocamldebug-coq: add some forgotten -IGravatar letouzey2009-05-26
* Temporary fixes in unification:Gravatar msozeau2009-05-24
* Moved and completed the history of Coq versions from theGravatar herbelin2009-05-24
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* Many fixes in unification:Gravatar msozeau2009-05-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 07:34:01 +0000