diff options
| author | Matthieu Sozeau | 2018-09-20 17:12:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-20 17:12:12 +0200 |
| commit | 7b6f1f0ed0872cd16d7d01683673fd9323122f30 (patch) | |
| tree | 2d3e6141d9dd38cc483df6a5ce6a59854519f047 /plugins | |
| parent | df1f5bcd406a87c77601942f21d16555a8f6086e (diff) | |
| parent | 69339f8fcfe3e5f3fa1c58feba6b0740c7e86538 (diff) | |
Merge PR #8297: Fix #7754: universe declarations on mutual inductives
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bbc0a37c69..fd2d90e9cf 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((CAst.make @@ relnames.(i)), None), + ((CAst.make @@ relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1499,14 +1499,14 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1521,7 +1521,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = |