diff options
| author | Emilio Jesus Gallego Arias | 2019-08-18 20:27:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-19 23:03:45 +0200 |
| commit | a74e055acf48583c6fece5d22c805736679376b2 (patch) | |
| tree | bc86b65608590013d7569b9585cd37029f2fa274 /plugins/funind | |
| parent | 7f9a08b98b1637291dda687fce92198a21ffc395 (diff) | |
[api] Move handling of variable implicit data to impargs
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
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 |