aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcorbinea2003-06-16 08:59:31 +0000
committercorbinea2003-06-16 08:59:31 +0000
commit49410249a3cbfc62e02b604b0e74fe1aa6db61f5 (patch)
tree707b85bc6faa7207cf1edc5cbbe16fd7650d70c9
parenteedd33040777e1114fd3a9aa838496390ce94d06 (diff)
ground update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4169 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/first-order/g_ground.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 059ca69a6a..2e8929c55e 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -25,7 +25,7 @@ let ground_depth=ref 5
let _=
let gdopt=
- { optsync=false;
+ { optsync=true;
optname="ground_depth";
optkey=SecondaryTable("Ground","Depth");
optread=(fun ()->Some !ground_depth);