diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 12 |
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 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) |