From 6b2c23ce5cfd7c0e25e835b5b3cc77909f60e2fe Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Mon, 8 Dec 2014 11:58:13 +0100
Subject: Closing bug 3837

---
 plugins/funind/glob_term_to_relation.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4f308af5eb..5cbe32d594 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1353,6 +1353,16 @@ let do_build_inductive
      Then save the graphs and reset Printing options to their primitive values
   *)
   let rel_arities = Array.mapi rel_arity funsargs in
+  let rel_params_ids =
+    List.fold_left
+      (fun  acc (na,_,_) ->
+       match na with
+	 Anonymous -> acc
+       | Name id -> id::acc
+      )
+      []
+      rels_params
+  in
   let rel_params =
     List.map
       (fun (n,t,is_defined) ->
@@ -1370,7 +1380,7 @@ let do_build_inductive
       (fun (id,t) ->
 	 false,((Loc.ghost,id),
 		with_full_print
-		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
+		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
 	       )
       ))
       (rel_constructors)
-- 
cgit v1.2.3