diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index e17336a71a..7307075bea 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -1368,9 +1368,10 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = (clear [id]) in if tac <> [] then - ((id,((tclTHEN ((tclTHEN (shift_left) (mk_then tac))) - (intros_using [id])))) :: tactic, - compile id flag t' :: defs) + let id' = new_identifier () in + ((id',((tclTHEN ((tclTHEN (shift_left) (mk_then tac))) + (intros_using [id'])))) :: tactic, + compile id' flag t' :: defs) else (tactic,defs) |