aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index a047bf53c7..7afd7a0385 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -983,7 +983,10 @@ let rec mem_named_context id ctxt =
let compact_named_context_reverse sign =
let compact l decl =
- let (i1,c1,t1) = NamedDecl.to_tuple decl in
+ let (i1,c1,t1) = match decl with
+ | NamedDecl.LocalAssum (i,t) -> i,None,t
+ | NamedDecl.LocalDef (i,c,t) -> i,Some c,t
+ in
match l with
| [] -> [[i1],c1,t1]
| (l2,c2,t2)::q ->