diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 67ae85d648..f0e5c6256c 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1375,7 +1375,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1390,7 +1390,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) ++ fnl () ++ Cerrors.explain_exn e in |