Skip to content

Commit

Permalink
Remove one use of empty_env in ssr
Browse files Browse the repository at this point in the history
  • Loading branch information
Maxime Dénès committed Oct 30, 2018
1 parent 000bf66 commit 365f14b
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions plugins/ssr/ssrequality.ml
Original file line number Diff line number Diff line change
Expand Up @@ -433,15 +433,15 @@ let lz_coq_prod =

let lz_setoid_relation =
let sdir = ["Classes"; "RelationClasses"] in
let last_srel = ref (Environ.empty_env, None) in
let last_srel = ref None in
fun env -> match !last_srel with
| env', srel when env' == env -> srel
| Some (env', srel) when env' == env -> srel
| _ ->
let srel =
try Some (UnivGen.constr_of_global @@
Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
with _ -> None in
last_srel := (env, srel); srel
last_srel := Some (env, srel); srel

let ssr_is_setoid env =
match lz_setoid_relation env with
Expand Down

0 comments on commit 365f14b

Please sign in to comment.