diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /tactics/inv.ml | |
parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r-- | tactics/inv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 412954989..b346ed223 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -292,7 +292,7 @@ let error_too_many_names pats = str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++ str ".") let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with @@ -496,9 +496,10 @@ let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort Evd.empty k ++ + pr_sort sigma k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e |