aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-30 12:10:35 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-30 12:11:04 +0200
commite6c41b96a5ea9f8559acf176cdf997b05ccfb317 (patch)
treed0b596966abb0d69a37448c481d68140edc63bd7
parenteefda76f6f42674fb342e1aa5f1dcf29569a4806 (diff)
Fix bug 5550: "typeclasses eauto with" does not work with section variables.
-rw-r--r--tactics/class_tactics.ml1
-rw-r--r--test-suite/bugs/closed/5550.v10
2 files changed, 11 insertions, 0 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d1ae85e7b..2c911addf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -593,6 +593,7 @@ let make_hints g st only_classes sign =
List.fold_left
(fun hints hyp ->
let consider =
+ not only_classes ||
let open Context.Named.Declaration in
try let t = Global.lookup_named (get_id hyp) |> get_type in
(* Section variable, reindex only if the type changed *)
diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v
new file mode 100644
index 000000000..bb1222489
--- /dev/null
+++ b/test-suite/bugs/closed/5550.v
@@ -0,0 +1,10 @@
+Section foo.
+
+ Variable bar : Prop.
+ Variable H : bar.
+
+ Goal bar.
+ typeclasses eauto with foobar.
+ Qed.
+
+End foo.