diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 7d43f1986f..61632e388e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -859,8 +859,9 @@ END let eq_constr x y = Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes evd x y with + match EConstr.eq_constr_universes env evd x y with | Some _ -> Proofview.tclUNIT () | None -> Tacticals.New.tclFAIL 0 (str "Not equal") end diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b6bac1a14e..99bb8440c6 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -90,7 +90,7 @@ let lookup_map map = let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in let c = EConstr.Unsafe.to_constr c0 in - EConstr.of_constr (kl (create_clos_infos ~evars all env) + EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ()) (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));; let protect_tac map = diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index e3941c1c5d..c3b6a7c59f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -178,7 +178,7 @@ GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - Vernacexpr.VernacUnsetOption (["Printing"; "Implicit"; "Defensive"]) + Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) ] ] ; END |