diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6d00e8d9f..c648939bb 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -191,9 +191,9 @@ let empty_seq depth= depth=depth} let expand_constructor_hints = - list_map_append (function + List.map_append (function | IndRef ind -> - list_tabulate (fun i -> ConstructRef (ind,i+1)) + List.tabulate (fun i -> ConstructRef (ind,i+1)) (Inductiveops.nconstructors ind) | gr -> [gr]) |