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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/classes.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
2 files changed, 3 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 075d89d0df..d5f5656e1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -28,9 +28,7 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) -open Decl_kinds - -let set_typeclass_transparency c local b = +let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -527,7 +525,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 84f437f640..88f87cdd0b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -169,7 +169,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = |