diff options
| author | Emilio Jesus Gallego Arias | 2019-06-11 02:16:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:14 +0200 |
| commit | 75e7c5b596d2a3e9b54e84788a15299568792584 (patch) | |
| tree | 6b326ec3279535bcad3f5bcbe0080679b2621dfb /vernac/declareObl.ml | |
| parent | 0ad30b6fce3eb757d06808e160a4c92e45686072 (diff) | |
[equations] [proof] Remove duplicate shrink function.
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
Diffstat (limited to 'vernac/declareObl.ml')
| -rw-r--r-- | vernac/declareObl.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 71215d2a3e..30aa347692 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -95,6 +95,7 @@ let decompose_lam_prod c ty = in aux Context.Rel.empty c ty +(* XXX: What's the relation of this with Abstract.shrink ? *) let shrink_body c ty = let ctx, b, ty = match ty with |