aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-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
* 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
* Fixing bug 2129 (evar introduced to remember an ambiguous projectionGravatar 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
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
* 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
* 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
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar msozeau2009-06-11
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
* Change unification with sort constraints to not use the kernelGravatar msozeau2009-06-01
* Properly catch sort constraint inconsistency exception inGravatar msozeau2009-05-28
* Populate the sort constraints set correctly during unification. Add aGravatar msozeau2009-05-27
* Temporary fixes in unification:Gravatar msozeau2009-05-24
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
* Many fixes in unification:Gravatar msozeau2009-05-20
* Fix in canonical structure resolution: [check_conv_record] may returnGravatar msozeau2009-05-19
* Remove camlp4-specific exception handlingGravatar msozeau2009-05-19
* Minor unification changes:Gravatar msozeau2009-05-18
* (Tentative to) add Canonical Structure resolution to the regularGravatar msozeau2009-05-16
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* fix a bug in canonical structures (bug found and fixed by Cyril)Gravatar barras2009-05-09
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* - New cleaning phase for the entry points of pretyping.mlGravatar herbelin2009-04-24
* fixed CBV strategy: it was too eager on terms likeGravatar barras2009-04-21
* - Fix handling of clauses in setoid_rewrite to rewrite under bindersGravatar msozeau2009-04-17
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Backtrack on 12061 (type checking for bug #2084 too strong as soon as we useGravatar herbelin2009-04-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Fix obvious bug in evars_of_named_context.Gravatar msozeau2009-04-03
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Fix bug #2056 (discharge bug).Gravatar msozeau2009-03-28
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 01:38:51 +0000