aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extract_env.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r--plugins/extraction/extract_env.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b0f6301192..b59e3b608c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -147,7 +147,7 @@ let check_fix env sg cb i =
| Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
| CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
| _ -> raise Impossible)
- | Undef _ | OpaqueDef _ -> raise Impossible
+ | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible
let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
Array.equal Name.equal na1 na2 &&