aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-10-25Merge remote-tracking branch 'github/pr/333' into v8.5Maxime Dénès
2016-10-22Remove incorrect assertion in cbn (bug #4822).Guillaume Melquiond
2016-10-22Fix a bug in error printing of unif constraintsMatthieu Sozeau
2016-10-21Revert "unification.ml: fix for bug #4763, unif regression"Maxime Dénès
2016-10-20A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Hugo Herbelin
2016-10-17Fixing to #3209 (Not_found due to an occur-check cycle).Hugo Herbelin
2016-10-17Fixing a missing constraint in consider_remaining_unif_constraints.Hugo Herbelin
2016-10-06evarconv.ml: Fix bug #4529, primproj unfoldingMatthieu Sozeau
2016-10-06w_merge: Add a comment about the (List.rev evars)Matthieu Sozeau
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu Sozeau
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-10Fixing #5077 (failure on typing a fixpoint with evars in its type).Hugo Herbelin
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
2016-06-27Refine fix for bug #4097, avoid proj expansionMatthieu Sozeau
2016-06-27More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:08:50 +0000