diff options
| author | Gaëtan Gilbert | 2019-08-23 23:06:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-08-23 23:06:41 +0200 |
| commit | 2c36189fb8c433fa1d3adff4ea2c52a7b1ff29cc (patch) | |
| tree | 4a201b720331128dfe60157057a8b95f250389b4 /vernac/classes.ml | |
| parent | b0a9cbeaf0530533008aa99246164b2bad896c5a (diff) | |
| parent | 451acd6ca6a9ce5b86622fb42085eb19e23d6665 (diff) | |
Merge PR #10665: [api] Move handling of variable implicit data to impargs
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files changed, 2 insertions, 4 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 |