diff options
| author | Pierre-Marie Pédrot | 2014-11-20 21:31:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-20 21:31:17 +0100 |
| commit | ec116774b1311d61f06ae9998dc5730f7c6f2f20 (patch) | |
| tree | 6ecfda048c7ee757e890f02027369129139d4cb8 | |
| parent | 9295b3dbacd124dde8cf53479822a1b3bbe4d967 (diff) | |
Fixing the previous commit. We had to normalize evars first.
| -rw-r--r-- | tactics/tacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 39070436e5..ac2255488b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2349,6 +2349,7 @@ let _ = | [c, _] -> c | _ -> assert false in + let ans = Reductionops.nf_evar sigma ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) |