aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2015-02-23Compensating 6fd763431 on postponing subtyping evar-evar problems.Hugo Herbelin
2015-02-23Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable...Hugo Herbelin
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
2015-02-23Fixing occur-check which was too strong in unification.ml.Hugo Herbelin
2015-02-21Fixing bug #3071.Pierre-Marie Pédrot
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-02-21Removing need for ensure_evar_independent by passing a force flag to is_const...Hugo Herbelin
2015-02-19When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Hugo Herbelin
2015-02-16Remove some dead code and add test-suite file.Matthieu Sozeau
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-02-15Fix 'don't expose cases' in cbnPierre Boutillier
2015-02-15Fixing bug #3490.Pierre-Marie Pédrot
2015-02-15Fixing bug #3916.Pierre-Marie Pédrot
2015-02-14Univs: fix bug #3755. We were missing refreshements of universes inMatthieu Sozeau
2015-02-12Fixing #3997 (occur-check in the presence of primitive projections, patchHugo Herbelin
2015-02-11Fixing bug #3900.Pierre-Marie Pédrot
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-19Making unification of LetIn's expressions more consistent (see #3920).Hugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-12Not "Setting ?n=?p order to ?p:=?n to see if it solves someHugo Herbelin
2015-01-08Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-07Reverting the tentative try to restore the use of second-orderHugo Herbelin
2015-01-06Propagating the relaxing of filtering started in 48509b6, fixed inHugo Herbelin
2015-01-06Fixing old filter bug in second_order_matching.Hugo Herbelin
2015-01-03Fixing 48509b61 which improved unification as expected but actuallyHugo Herbelin
2015-01-03Tentatively trying to restore the use of second-order typed-basedHugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo Herbelin
2014-12-19When pretyping [uconstr] closures, don't use the local Ltac variable environm...Arnaud Spiwack
2014-12-19Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Hugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-12-15Tentatively starting to use heuristics for evar-evar resolution: firstHugo Herbelin
2014-12-15New try on Fixing an evar_map bug revealed by commit 603b66f81 onHugo Herbelin
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-11Commit not ready. Sorry.Hugo Herbelin
2014-12-11Added a CannotSolveConstraint unification error and made experimentsHugo Herbelin
2014-12-11Fine-tuning unification error (using OccurCheck in evarconv).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:19:37 +0000