From 9a9a2c9c330189a677d99d1e71890dcb238c53b3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Sep 2006 13:15:15 +0000
Subject: Suite commit 9110 (uniformisation position notation dans les blocs
 inductifs)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9114 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/name_to_ast.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index b06ba1992d..6195caa472 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
-- 
cgit v1.2.3