From 442feb2c07f8f5824e814bba504f02c2742637e2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:09 +0000
Subject: Vernacexpr is now a mli-only file, locality stuff now in locality.ml

 Adds a directory ./intf for pure interfaces.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/g_ground.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 48bb87214a..a5ee551a52 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -59,7 +59,7 @@ let (set_default_solver, default_solver, print_default_solver) =
 VERNAC COMMAND EXTEND Firstorder_Set_Solver
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
-      (Vernacexpr.use_section_locality ())
+      (Locality.use_section_locality ())
       (Tacinterp.glob_tactic t) ]
 END
 
-- 
cgit v1.2.3