diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:02:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
| commit | 3ca949d4069308cf71c8f22b8dfc89e95a3834c1 (patch) | |
| tree | e62c966cf36841deeba474bd4b722881ed9f39b2 /pretyping/reductionops.ml | |
| parent | b6e39ade125862ba41ca17b06b8e35726b9b0d7d (diff) | |
Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.
Diffstat (limited to 'pretyping/reductionops.ml')
0 files changed, 0 insertions, 0 deletions