diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 17:45:04 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 17:55:47 +0200 |
| commit | 2adff76c5466734c633923e768c9dcbdc6f28c86 (patch) | |
| tree | aca997d04a076e09ce62929415cd66820a5c92d3 /plugins/funind/glob_term_to_relation.ml | |
| parent | 4a73e6b2bfb75451bcda7c74cf7478726a459799 (diff) | |
Add corresponding field in `VernacInductive`.
Makes sure not to generate inductive schemes of assumed positive types.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 065c12a2d..b4febba66 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1424,7 +1424,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1435,7 +1435,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1450,7 +1450,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in |