diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-12 14:44:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-12 14:44:33 +0200 |
| commit | c464965df350ab5007d2a1c0d6e625d119abf650 (patch) | |
| tree | d6651eb90ab000743ad79863706aba9e3c1a96f6 /tools | |
| parent | ab4bce38a7c0d08d1ebff70c4115b7c1d8e8be88 (diff) | |
Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").
This is a quick fix. Code should be made nicer along these lines:
- try to pass the name of the variable created by "mkletin_goal" in
the monad using "refine_one";
- use a disjunctive type of "inhyps" to indicate when it is
meaningful, rather than using [].
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions