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 0ac120327..1e4267421 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -475,7 +475,7 @@ let raw_inversion inv_kind indbinding id status names gl = (fun id -> (tclTHEN (apply_term (mkVar id) - (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns)) + (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) reflexivity))]) gl |