diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 |
3 files changed, 7 insertions, 6 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/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 7bddbc994f..446026c4c8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -295,8 +295,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) ~name:new_princ_name ~hook_data ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) - UnivNames.empty_binders - entry [] in + ~ubind:UnivNames.empty_binders + ~impargs:[] + entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c7dfe69fb1..e08ad9af3a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1517,7 +1517,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1532,7 +1532,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)}) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in |