aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 5a4cda54b2..14a3acad57 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -76,7 +76,7 @@ VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
let open Attributes in
set_default_solver
- (Locality.make_section_locality atts.locality)
+ (Locality.make_section_locality (only_locality atts))
(Tacintern.glob_tactic t)
}
END