diff options
| author | Gaëtan Gilbert | 2020-02-21 14:41:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-21 14:41:42 +0100 |
| commit | 94fcc24a7a81253e3ede8661fc12401bbebdd14f (patch) | |
| tree | 842e4bf529654690968734193514b9305186a590 /kernel/nativeconv.ml | |
| parent | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (diff) | |
Tactic_matching.pattern_match_term: remove ignored "refresh" argument
It's been ignored since the introduction of universe polymorphism.
Diffstat (limited to 'kernel/nativeconv.ml')
0 files changed, 0 insertions, 0 deletions