aboutsummaryrefslogtreecommitdiff
path: root/proofs/evar_refiner.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 /proofs/evar_refiner.ml
parentad5aea737ecc639c31dda84322b3550a4d380b47 (diff)
Rename TranspState into TransparentState.
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r--proofs/evar_refiner.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fb42a9cebe..6c4193c66b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -37,7 +37,7 @@ let define_and_solve_constraints evk c env evd =
match
List.fold_left
(fun p (pbty,env,t1,t2) -> match p with
- | Success evd -> Evarconv.evar_conv_x TranspState.full env evd pbty t1 t2
+ | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2
| UnifFailure _ as x -> x) (Success evd)
pbs
with