diff options
Diffstat (limited to 'plugins/funind/rawterm_to_relation.ml')
| -rw-r--r-- | plugins/funind/rawterm_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index 4bd0385ca..607734f22 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/rawterm_to_relation.ml @@ -1364,7 +1364,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.build_mutual rel_inds)) true + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true with | UserError(s,msg) as e -> let _time3 = System.get_time () in |