diff options
Diffstat (limited to 'contrib/interface/name_to_ast.ml')
-rw-r--r-- | contrib/interface/name_to_ast.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 5180bdad2..668a581e1 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 = |