diff options
| author | Gaëtan Gilbert | 2020-02-12 13:54:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-13 15:12:01 +0100 |
| commit | 3af570b60e6912d2eb906ce86a3df3b8ecca675c (patch) | |
| tree | 17005ee530a8447dc8d58b5e58ec23edebd5711e /plugins/funind | |
| parent | e76b9da873d2e690e9dd24ed36ecec505676651e (diff) | |
Don't duplicate the inductive keyword for each block elt when parsing
Diffstat (limited to 'plugins/funind')
| -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 84f09c385f..fdbad2ab9e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1512,12 +1512,12 @@ 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,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1527,12 +1527,12 @@ 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,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in |