From 5a87d97bd8bce29d3c94bd40e4ab03c4c7c098a8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Sep 2006 12:30:52 +0000
Subject: Ajout possibilité clause "where" dans co-points fixes (+
 uniformisation position notation dans les blocs inductifs et récursifs)

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

(limited to 'contrib/funind')

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index a24e5845b5..5f09b3590a 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1194,11 +1194,10 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors = 
-    (dummy_loc,relnames.(i)),
-    None,
+    ((dummy_loc,relnames.(i)),
     rel_params,
     rel_arities.(i),
-    ext_rel_constructors
+    ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
   let rel_inds = Array.to_list ext_rel_constructors in 
-- 
cgit v1.2.3