diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-05 11:57:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-23 22:13:57 +0100 |
| commit | 45a411377244da33111cf5d7002df70de912bc64 (patch) | |
| tree | c01b496bbe54b7299fe8e7cafa279fcc55ddf05b /tools | |
| parent | 8f5d447769a41cd251701272a6ff71a7a20de658 (diff) | |
Factorizing/unifying code in dealing with binders.
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions