From c310dc5efedcbc31d74d568e5bb4bfecf458c25b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Sep 2014 21:08:22 +0200
Subject: Removing antiquotations in Tauto.

---
 tactics/tauto.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index a05b02254b..346f560f8d 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -80,6 +80,10 @@ let _ =
 
 (** Test *)
 
+let make_lfun l =
+  let fold accu (id, v) = Id.Map.add (Id.of_string id) v accu in
+  List.fold_left fold Id.Map.empty l
+
 let is_empty ist =
   if is_empty_type (assoc_var "X1" ist) then
     <:tactic<idtac>>
@@ -259,7 +263,7 @@ let rec tauto_intuit flags t_reduce solver =
   let t_axioms = tacticIn (axioms flags)
   and t_simplif = tacticIn (simplif flags)
   and t_is_disj = tacticIn (is_disj flags) in
-  let lfun = Id.Map.singleton (Id.of_string "t_solver") solver in
+  let lfun = make_lfun [("t_solver", solver)] in
   let ist = { default_ist () with lfun = lfun; } in
   let vars = [Id.of_string "t_solver"] in
   (vars, ist, <:tactic<
-- 
cgit v1.2.3