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 | |
| parent | 85aebaa1a28b0f2bb2848d4e6c16c9b990648b48 (diff) | |
| parent | ca91aa115378ec24a5be34ba506b071b4662df4b (diff) | |
Merge PR #11847: Properly thread let-bindings in Funind principle construction.
Reviewed-by: Matafou
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11846.v | 16 |
2 files changed, 18 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 diff --git a/test-suite/bugs/closed/bug_11846.v b/test-suite/bugs/closed/bug_11846.v new file mode 100644 index 0000000000..53517e7703 --- /dev/null +++ b/test-suite/bugs/closed/bug_11846.v @@ -0,0 +1,16 @@ +Require Import FunInd. + +Inductive tree : Type := +| Node : unit -> tree. + +Definition height (s : tree) : unit := +match s with +| Node h => h +end. + +Definition bal : forall l, let h := height l in tree := fun l => + let h := height l in + Node h. + +Set Warnings "+all". +Functional Scheme bal_ind := Induction for bal Sort Prop. |