aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Made unification patch 12268 even more ad hoc (if evars remain in aGravatar herbelin2009-08-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 00:24:29 +0000