diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_12566_1.v | 16 | ||||
| -rw-r--r-- | vernac/comHints.ml | 21 |
2 files changed, 31 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v new file mode 100644 index 0000000000..22d95949bb --- /dev/null +++ b/test-suite/bugs/closed/bug_12566_1.v @@ -0,0 +1,16 @@ + +Class C (n:nat) := c{}. + +Instance c0 : C 0 := {}. + +Definition x := 0. + +Opaque x. + +Type _ : C x. +(* this is maybe wrong behaviour, if it changes just update the test *) + +Hint Opaque x : typeclass_instances. +Transparent x. + +Fail Type _ : C x. diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 0e3e3c61a9..051560fb63 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -9,6 +9,7 @@ (************************************************************************) open Util +open Names (** (Partial) implementation of the [Hint] command; some more functionality still lives in tactics/hints.ml *) @@ -61,7 +62,7 @@ let project_hint ~poly pri l2r r = cb in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c)) + (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) let warn_deprecated_hint_constr = CWarnings.create ~name:"fragile-hint-constr" ~category:"automation" @@ -70,6 +71,16 @@ let warn_deprecated_hint_constr = "Declaring arbitrary terms as hints is fragile; it is recommended to \ declare a toplevel constant instead") +(* Only error when we have to (axioms may be instantiated if from functors) + XXX maybe error if not from a functor argument? + *) +let soft_evaluable = + let open GlobRef in + function + | ConstRef c -> EvalConstRef c + | VarRef id -> EvalVarRef id + | (IndRef _ | ConstructRef _) as r -> Tacred.error_not_evaluable r + let interp_hints ~poly h = let env = Global.env () in let sigma = Evd.from_env env in @@ -88,7 +99,7 @@ let interp_hints ~poly h = Dumpglob.add_glob ?loc:r.CAst.loc gr; gr in - let fr r = Tacred.evaluable_of_global_reference env (fref r) in + let fr r = soft_evaluable (fref r) in let fi c = let open Hints in let open Vernacexpr in @@ -135,7 +146,7 @@ let interp_hints ~poly h = "ind"; List.init (Inductiveops.nconstructors env ind) (fun i -> let c = (ind, i + 1) in - let gr = Names.GlobRef.ConstructRef c in + let gr = GlobRef.ConstructRef c in ( empty_hint_info , Declareops.inductive_is_polymorphic mib , true @@ -147,9 +158,7 @@ let interp_hints ~poly h = let pat = Option.map (fp sigma) patcom in let l = match pat with None -> [] | Some (l, _) -> l in let ltacvars = - List.fold_left - (fun accu x -> Names.Id.Set.add x accu) - Names.Id.Set.empty l + List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in let env = Genintern.{(empty_glob_sign env) with ltacvars} in let _, tacexp = Genintern.generic_intern env tacexp in |