aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
* Use camlp4 to accept some specific non-exhaustive patterns in groebnerGravatar letouzey2009-07-20
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* Typo in a commentGravatar letouzey2009-07-20
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Allow coqdoc comments inside definition bodies.Gravatar msozeau2009-07-09
* Correction bug 2134.Gravatar soubiran2009-07-09
* Fixed bug #2116 ("simpl" created ill-typed term while acceptingGravatar herbelin2009-07-08
* Don't use recent ocaml tolerance for pattern "ProjectVar _" whenGravatar herbelin2009-07-08
* Simplify addition of hints to a hint_db. Rebuild the dnet associatedGravatar msozeau2009-07-08
* Use user-given implicits from the arity in inductive definitions.Gravatar msozeau2009-07-08
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Add heuristic based on non-linearity of evars to determine whether anGravatar herbelin2009-07-08
* Fixed anomaly when trying to load non existing file starting with "./" or "../".Gravatar herbelin2009-07-08
* Fixing bug 2129 (evar introduced to remember an ambiguous projectionGravatar herbelin2009-07-08
* Completing support for F5=About by adding About to the state-preserving comma...Gravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* change in the order of unification constraints solving (for canonical structu...Gravatar amahboub2009-07-06
* repport of commit r12221Gravatar jforest2009-07-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 11:22:13 +0000