diff options
| author | Maxime Dénès | 2018-10-30 12:00:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:10:02 +0100 |
| commit | 365f14bdb87f6f323d635267f69f507b540ef2a8 (patch) | |
| tree | a3b29564bf17adebc44fc31ab23f99012cdcc88b | |
| parent | 000bf6684a872bc29191807c29a64011f7f82350 (diff) | |
Remove one use of empty_env in ssr
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index c04ced4ab4..036b20bfcd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -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 |