diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 1 |
3 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730ae48393..a836335d4d 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1600,7 +1600,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( [CAst.make @@ Name a; CAst.make @@ Name b], - Constrexpr.Default Decl_kinds.Explicit, + Constrexpr.Default Glob_term.Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, [ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6eb8c42d1d..ddd6ecfb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt = | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt)], + Constrexpr.Default Explicit, rt)], CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index d36d86a65b..fbf63c69dd 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -4,7 +4,6 @@ open Glob_term open CErrors open Util open Names -open Decl_kinds (* Some basic functions to rebuild glob_constr |