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 /pretyping/coercion.ml | |
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 'pretyping/coercion.ml')
0 files changed, 0 insertions, 0 deletions