diff options
| author | Pierre-Marie Pédrot | 2014-09-08 21:08:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-08 21:08:22 +0200 |
| commit | c310dc5efedcbc31d74d568e5bb4bfecf458c25b (patch) | |
| tree | 40f1ed7f3c526be04ef5561f89aee49f58d11f85 | |
| parent | 51d38d0892eae4a253356e52614da6dee6513e9e (diff) | |
Removing antiquotations in Tauto.
| -rw-r--r-- | tactics/tauto.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
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< |