diff options
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cf603e8fde..047cb0b74b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2934,7 +2934,9 @@ let symmetry_red allowred gl = let hdcncls = string_of_inductive hdcncl in begin try - (apply (pf_parse_const gl ("sym_"^hdcncls)) gl) + tclTHEN + (convert_concl_no_check concl DEFAULTcast) + (apply (pf_parse_const gl ("sym_"^hdcncls))) gl with _ -> let symc = match args with | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) |