aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/proof_using.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/proof_using.ml')
-rw-r--r--vernac/proof_using.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index ffe99cfd8..8422baf57 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -51,7 +51,7 @@ let rec process_expr env e ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
| SsType -> set_of_type env ty
- | SsSingl (_,id) -> set_of_id env id
+ | SsSingl { CAst.v = id } -> set_of_id env id
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)