aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-11 22:07:12 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-11 22:07:12 +0200
commitad86932abc23df9139065d453771a190df365928 (patch)
tree5f39f4df556b2359a64907847f801a355032b5ba /tactics
parentae42e00f886f7c2ef743e2fdd58c55b5c3acdd87 (diff)
Oopps.. fixed the .ml not the .ml4
Diffstat (limited to 'tactics')
-rw-r--r--tactics/g_rewrite.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 5c46fdf2a..57dba7d61 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -104,7 +104,7 @@ END
(* By default the strategy for "rewrite_db" is top-down *)
-let db_strat db = StratUnary ("topdown", StratHints (false, db))
+let db_strat db = StratUnary (Topdown, StratHints (false, db))
let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
let cl_rewrite_clause_db =