aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
* Fix bug introduced by last revision, subtac_cases was returning theGravatar msozeau2009-06-29
* Raise an error and not an anomaly if a rewrite is attempted on aGravatar msozeau2009-06-28
* Abstract the tycon by the matched terms when turning them into variablesGravatar msozeau2009-06-28
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
* propagation sur le trunk du commit 12101 Gravatar soubiran2009-06-26
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
* Correct treatment of dependent products in signatures: create the evarsGravatar msozeau2009-06-22
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
* documented a bug of pattern unification with metasGravatar barras2009-06-22
* made several occurrences of (eapply ...; eauto) not rely on the lack of patte...Gravatar barras2009-06-22
* Report de la révision #12200 (bug #2125)Gravatar notin2009-06-22
* remove some unused functions (which are part of a soon-to-be obsoleteGravatar vgross2009-06-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-25 06:01:24 +0000