diff options
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b5a5f984fc..a403832fff 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -731,7 +731,8 @@ let rec intern_atomic lf ist x = TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> TacChange (Option.map (intern_constr_occurrence ist) occl, - (if occl = None then intern_type ist c else intern_constr ist c), + (if occl = None & cl.onhyps = None & cl.concl_occs = [] + then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) (* Equivalence relations *) |