aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* Fixes to make Ynot compile with the trunk:Gravatar msozeau2009-03-20
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* On passe les last_mods (un des champs de Evd.evar_defs) de listGravatar aspiwack2009-02-20
* On ne met plus rien dans les last_mods tant que conv_pbs est vide.Gravatar aspiwack2009-02-20
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* memoized is_ground_envGravatar barras2009-02-09
* pushed evar reduction in kernelGravatar barras2009-02-06
* From v8.2 to trunk:Gravatar herbelin2009-02-06
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 11:27:14 +0000