Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 3 insertions, 3 deletions

diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index b06ba199..9a503cfb 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), None,
+  (((dummy_loc,basename sp),
    convert_env(List.rev params),
    (extern_constr true envpar arity),
-   convert_constructors envpar cstrnames cstrtypes);;
+   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
@@ -149,7 +149,7 @@ let make_definition_ast name c typ implicits =
 let constant_to_ast_list kn =
   let cb = Global.lookup_constant kn in
   let c = cb.const_body in
-  let typ = cb.const_type in
+  let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in
   let l = implicits_of_global (ConstRef kn) in
   (match c with
       None ->