diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 8 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index f0e5c6256c..7e9ba3f8ea 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1370,12 +1370,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) , b, c , None, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1385,12 +1385,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) , b, c , None, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ Cerrors.explain_exn e in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 5180bdad27..668a581e1d 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -109,7 +109,7 @@ let convert_one_inductive sp tyi = let sp = sp_of_global (IndRef (sp, tyi)) in (((false,(dummy_loc,basename sp)), convert_env(List.rev params), - Some (extern_constr true envpar arity), None, + Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw , Constructors (convert_constructors envpar cstrnames cstrtypes)), None);; (* This function converts a Mutual inductive definition to a Coqast.t. @@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib = let _, l = Array.fold_right (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in - VernacInductive (mib.mind_finite, false, l) + VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l) :: (implicit_args_to_ast_list sp mipv);; let constr_to_ast v = diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 71cef59e2f..c8684a9a0e 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1984,7 +1984,7 @@ let rec xlate_vernac = (* xlate_formula (Option.get c1), record_constructor, *) (* build_record_field_list field_list) *) | VernacInductive (isind, _, lmi) -> - let co_or_ind = if isind then "Inductive" else "CoInductive" in + let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in let strip_mutind = function (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) -> CT_ind_spec |