diff options
| -rw-r--r-- | plugins/ltac/g_class.mlg | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 11 | ||||
| -rw-r--r-- | tactics/hints.mli | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4527.v | 1 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 4 | ||||
| -rw-r--r-- | vernac/classes.ml | 13 |
9 files changed, 21 insertions, 24 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 3f2fabeeee..049a699cbd 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] } + typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8e9a2e114b..fa64c21d1e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -265,8 +265,8 @@ let apply_inference_hook hook env sigma frozen = match frozen with let apply_heuristics env sigma fail_evar = (* Resolve eagerly, potentially making wrong choices *) - try solve_unif_constraints_with_heuristics - ~flags:(default_flags_of (Typeclasses.classes_transparent_state ())) env sigma + let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in + try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> let e = CErrors.push e in if fail_evar then iraise e else sigma diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a3620f4081..5f003b74bd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -33,7 +33,8 @@ open Hints module NamedDecl = Context.Named.Declaration -(** Hint database named "typeclass_instances", now created directly in Auto *) +(** Hint database named "typeclass_instances", created in prelude *) +let typeclasses_db = "typeclass_instances" (** Options handling *) diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index a6922213d0..c950e3de3d 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -13,6 +13,8 @@ open Names open EConstr +val typeclasses_db : string + val catchable : exn -> bool val set_typeclasses_debug : bool -> unit diff --git a/tactics/hints.ml b/tactics/hints.ml index 85d75f1010..0daf57ae84 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -738,16 +738,7 @@ module Hintdbmap = String.Map type hint_db = Hint_db.t -(** Initially created hint databases, for typeclasses and rewrite *) -let typeclasses_db = "typeclass_instances" -let rewrite_db = "rewrite" - -let auto_init_db = - Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true) - (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true) - Hintdbmap.empty) - -let searchtable = Summary.ref ~name:"searchtable" auto_init_db +let searchtable = Summary.ref ~name:"searchtable" Hintdbmap.empty let statustable = Summary.ref ~name:"statustable" KNmap.empty let searchtable_map name = diff --git a/tactics/hints.mli b/tactics/hints.mli index dd2c63d351..a069e53852 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -277,11 +277,6 @@ val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> de val make_db_list : hint_db_name list -> hint_db list -(** Initially created hint databases, for typeclasses and rewrite *) - -val typeclasses_db : hint_db_name -val rewrite_db : hint_db_name - val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic (** Use around toplevel calls to hint-using tactics, to enable the tracking of non-imported hints. Any tactic calling [run_hint] must be wrapped this diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v index 4f8a8dd272..dfb07520f1 100644 --- a/test-suite/bugs/closed/bug_4527.v +++ b/test-suite/bugs/closed/bug_4527.v @@ -10,6 +10,7 @@ Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. Require Coq.Init.Datatypes. +Require Import Coq.Init.Tactics. Import Coq.Init.Notations. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index af4632161e..497cf2550b 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -332,3 +332,7 @@ Tactic Notation "assert_succeeds" tactic3(tac) := assert_succeeds tac. Tactic Notation "assert_fails" tactic3(tac) := assert_fails tac. + +Create HintDb rewrite discriminated. +Hint Variables Opaque : rewrite. +Create HintDb typeclass_instances discriminated. diff --git a/vernac/classes.ml b/vernac/classes.ml index 1981e24ae4..6ce2a3f0a5 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -21,6 +21,7 @@ open Globnames open Constrintern open Constrexpr open Context.Rel.Declaration +open Class_tactics module RelDecl = Context.Rel.Declaration (*i*) @@ -38,12 +39,15 @@ let () = Goptions.(declare_bool_option { optwrite = (fun b -> refine_instance := b) }) -let typeclasses_db = "typeclass_instances" - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) - + +let classes_transparent_state () = + try + Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db) + with Not_found -> TransparentState.empty + let () = Hook.set Typeclasses.add_instance_hint_hook (fun inst path local info poly -> @@ -55,8 +59,7 @@ let () = (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst'])) ()); Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; - Hook.set Typeclasses.classes_transparent_state_hook - (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) + Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let intern_info {hint_priority;hint_pattern} = let env = Global.env() in |