aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tactics/term_dnet.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 901f366ec..7567cfa30 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -221,7 +221,8 @@ struct
let terminal = function
| (DRel | DSort | DNil | DRef _) -> true
- | _ -> false
+ | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ ->
+ false
let compare t1 t2 = compare dummy_cmp t1 t2