aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-06-13evar_conv: Refine occur_rigidlyMatthieu Sozeau
2016-06-12Minor simplification in evarconv.Hugo Herbelin
2016-06-12Reserve exception "ConversionFailed" in unification for failure ofHugo Herbelin
2016-06-12Protecting eta-expansion in evarconv.ml against ill-typed problems.Hugo Herbelin
2016-06-09Fixing #4644 (regression of unification on evar-evar problems with a match).Hugo Herbelin
2016-06-09Minor simplification in evarconv.ml.Hugo Herbelin
2016-06-09Reverting dbdff037 which does not seem to prevent to have #3638 fixedHugo Herbelin
2016-05-12Small optimization in evar resolution.Pierre-Marie Pédrot
2016-05-03Use the canonical name when looking for an eliminator (bug #4670).Guillaume Melquiond
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-03-25Fix a bug in Program coercion codeMatthieu Sozeau
2016-03-17Fix #4623: set tactic too weak with universes (regression)Maxime Dénès
2016-03-16Fix incorrect behavior of CS resolutionMatthieu Sozeau
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-03Optimizing the computation of frozen evars.Pierre-Marie Pédrot
2016-02-03Opacifying the type of evar naming structure in Evd.Pierre-Marie Pédrot
2016-02-03More compact representation for evar resolvability flag.Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-23Fix bug #4519: oops, global shadowed local universe level bindings.Matthieu Sozeau
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-12-17(Partial) fix for bug #4453: raise an error instead of an anomaly.Matthieu Sozeau
2015-12-11Optimize occur_evar_upto_types, avoiding repeateadly looking into theMatthieu Sozeau
2015-12-02Add an option to deactivate compatibility printing of primitiveMatthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-25Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Hugo Herbelin
2015-11-24Fixing an old typo in Retyping, found by Matej.Hugo Herbelin
2015-11-22Fixing a vm_compute bug in the presence of let-ins among theHugo Herbelin
2015-11-22Fixing a bug of adjust_subst_to_rel_context.Hugo Herbelin
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-11Ensure that conversion is called on terms of the same type inMatthieu Sozeau
2015-11-11Fix bug #3998: when using typeclass resolution for conversion, allowMatthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-04Univs: compatibility with 8.4.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 09:32:07 +0000