Closing bug 3837

1 files changed, 11 insertions, 1 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4f308af5e..5cbe32d59 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)