diff options
| author | Pierre Courtieu | 2020-03-20 13:59:10 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2020-03-20 13:59:10 +0100 |
| commit | 06b820259989a59080d0dc68bf0c633994fe221f (patch) | |
| tree | 162e60b012680114ef2cf3d9cc85608196b27e62 /plugins/funind | |
| parent | 85aebaa1a28b0f2bb2848d4e6c16c9b990648b48 (diff) | |
| parent | ca91aa115378ec24a5be34ba506b071b4662df4b (diff) | |
Merge PR #11847: Properly thread let-bindings in Funind principle construction.
Reviewed-by: Matafou
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 275468ad3d..163645b719 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -63,14 +63,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in + let args,_ = decompose_prod_assum (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in let real_args = if princ_type_info.indarg_in_concl then List.tl args else args in Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl), - Term.compose_prod real_args (mkSort new_sort)) + Term.it_mkProd_or_LetIn (mkSort new_sort) real_args) in let new_predicates = List.map_i |