aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2009-07-08Completing support for F5=About by adding About to the state-preserving comma...herbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-07-06change in the order of unification constraints solving (for canonical structu...amahboub
2009-07-04repport of commit r12221jforest
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
2009-06-29Miscellaneous practical commits: herbelin
2009-06-29Fix bug introduced by last revision, subtac_cases was returning themsozeau
2009-06-28Raise an error and not an anomaly if a rewrite is attempted on amsozeau
2009-06-28Abstract the tycon by the matched terms when turning them into variablesmsozeau
2009-06-28Improve return predicate inference by making the return type dependentmsozeau
2009-06-26propagation sur le trunk du commit 12101 soubiran
2009-06-26Add doc for [Print Opaque Dependencies] and a better explanation for themsozeau
2009-06-22Correct treatment of dependent products in signatures: create the evarsmsozeau
2009-06-22Fixes for r12197, the refined evars were not returned in case fail_evarmsozeau
2009-06-22documented a bug of pattern unification with metasbarras
2009-06-22made several occurrences of (eapply ...; eauto) not rely on the lack of patte...barras
2009-06-22Report de la révision #12200 (bug #2125)notin
2009-06-22remove some unused functions (which are part of a soon-to-be obsoletevgross
2009-06-22clearing unused functionsvgross
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-18Try typeclass resolution in coercion if no solution can be found to amsozeau
2009-06-17Fallback on not using [fix_proto] if the right imports aren't there, the msozeau
2009-06-16Reimplementation of leibniz rewrite to control the instantiation of themsozeau
2009-06-15Allow anonymous instances again, with syntax [Instance: T] where Tmsozeau
2009-06-13Correct typo: -noglob takes no argument.msozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
2009-06-11When typing a non-dependent arrow, do not put the (anonymous) variablemsozeau
2009-06-10Accept more Unicode symbolsglondu
2009-06-10Use the projections for reflexivity, symmetry and transitivity proofs tomsozeau
2009-06-09Correct handling of the initial existentials from the goal and the onesmsozeau
2009-06-08Do a fixpoint on the result of typeclass search to force themsozeau
2009-06-08Change in UI behaviour : proof folding is now done by double clicking. Delay isvgross
2009-06-07File forgotten in commit 12171.herbelin
2009-06-07Partial simplification of undo mechanism, relying only on Courtieu'sherbelin
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2009-06-06Makefile made compatible with Solaris 10 (bug #2078, continued - seeherbelin
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
2009-06-06Fixing bug #2106 ("match" compilation with multi-dependent constructor).herbelin
2009-06-06Very-small-step policy changes to the library.herbelin
2009-06-06Applying Ian Lynagh's documentation fixes patch (see bug #2112)herbelin
2009-06-03Ensure the precondition of the partial function [list_chop] holdsmsozeau
2009-06-02Adding a regression test about Bauer's example on coq-club ofherbelin
2009-06-02Use Type instead of Set.msozeau
2009-06-02Backtrack on experimental unification with sort variables: it requires msozeau
2009-06-02Fix script file using the "Manual Implicit" flag.msozeau
2009-06-01## Lines starting with '## ' will be removed from the log message.msozeau
2009-06-01Change unification with sort constraints to not use the kernelmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 22:42:50 +0000