diff options
| -rw-r--r-- | tactics/equality.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 763ca14c3c..ee2c9c450e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1336,6 +1336,7 @@ let substConcl_RL_tac = (function | [Command eqn] -> (fun gls -> substConcl_RL (pf_interp_constr gls eqn) gls) + | [Constr c] -> substConcl_RL c | _ -> assert false) in fun eqn -> gentac [Command eqn] |