diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/interface/name_to_ast.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/interface/name_to_ast.ml')
-rw-r--r-- | contrib/interface/name_to_ast.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 6b17e739..0dc8f024 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -107,10 +107,10 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in let sp = sp_of_global (IndRef (sp, tyi)) in - (((dummy_loc,basename sp), + (((false,(dummy_loc,basename sp)), convert_env(List.rev params), - (extern_constr true envpar arity), - convert_constructors envpar cstrnames cstrtypes), 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. It is obtained directly from print_mutual in pretty.ml. However, all @@ -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, l) + VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), l) :: (implicit_args_to_ast_list sp mipv);; let constr_to_ast v = |