From 8a1f5056e144c12e5e67aa7ac328cd65e730ede2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 5 Sep 2014 17:49:37 +0200
Subject: Fix parsing of "subterm(s)" strategy argument.

---
 tactics/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 5c2e3ec293..c545332edb 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1617,8 +1617,8 @@ let rec strategy_of_ast = function
   | StratUnary (f, s) -> 
     let s' = strategy_of_ast s in
     let f' = match f with
-      | "subterms" -> all_subterms
-      | "subterm" -> one_subterm
+      | "all_subterms" -> all_subterms
+      | "one_subterm" -> one_subterm
       | "innermost" -> Strategies.innermost
       | "outermost" -> Strategies.outermost
       | "bottomup" -> Strategies.bu
-- 
cgit v1.2.3