diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 6841ab0ec..89c6beb32 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names = in let refined id = let prf = mkApp (mkVar id, args) in - Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } + Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } in let neqns = List.length realargs in let as_mode = names != None in |