aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 1751c5d82d..e29a9edcd0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -479,7 +479,7 @@ let args_of_mconstr c = match kind_of_term c with
| _ -> anomaly "args_of_mconstr called with bad args"
let isMutConstruct c = match kind_of_term c with
- IsMutCase _ -> true | _ -> false
+ IsMutConstruct _ -> true | _ -> false
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
let destCase c = match kind_of_term c with