aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-19 08:12:28 +0100
committerPierre-Marie Pédrot2018-11-19 13:29:55 +0100
commit733cb74a2038ff92156b7209713fc2ea741ccca6 (patch)
treeee664936850ce6160d9e3fc3219b9dba7b7ea096 /pretyping/cases.ml
parentad5aea737ecc639c31dda84322b3550a4d380b47 (diff)
Rename TranspState into TransparentState.
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 647ef5092f..e02fb33276 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1698,7 +1698,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context !!env) in
let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
- begin match solve_simple_eqn (evar_conv_x TranspState.full) !!env sigma (None,ev,substl inst ev') with
+ begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
end;