aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/inductive.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 605405e353..b04c77ad86 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -525,8 +525,8 @@ let branches_specif renv c_spec ci =
Array.map
(fun t -> Lazy.force (spec_of_tree (lazy t)))
vra
- | Dead_code -> Array.create nca Dead_code
- | _ -> Array.create nca Not_subterm) in
+ | Dead_code -> Array.make nca Dead_code
+ | _ -> Array.make nca Not_subterm) in
List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
car