diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-12-08 11:58:13 +0100 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-12-08 13:34:19 +0100 |
| commit | 6b2c23ce5cfd7c0e25e835b5b3cc77909f60e2fe (patch) | |
| tree | b5bae38bae0f4cbe77a6e8f3d4394581a296e0ea /plugins/funind/glob_term_to_relation.ml | |
| parent | bdc5c300fc0c461a930b3766c9841d5c72f7947a (diff) | |
Closing bug 3837
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -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 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) |