Code

[wip] improve Elpi elaborator#169

Code

Draft

gares wants to merge 3 commits intomasterLPCIC/coq-elpi:masterfrom improve-elaboratorLPCIC/coq-elpi:improve-elaboratorCopy head branch name to clipboard

+145-45

Commits

Commits on Jul 30, 2020

• ut is not accompanied by a restriction propagation rule

  gares

  committed
  d0cb429

  Copy full SHA for d0cb429

Commits on Jul 31, 2020

• fix coercion.db-for doc & implementation

  gares

  committed
  35d78cd

  Copy full SHA for 35d78cd

• wip coercions

  gares

  committed
  724c661

  Copy full SHA for 724c661