diff options
| author | Matthieu Sozeau | 2015-09-24 10:51:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | 89cf845e1653c2f9b274d413561f10b7019d4858 (patch) | |
| tree | 21ab0e740b90ad2886a7271019813096433b126e | |
| parent | b969b459021fe70272baa85e83c12268baf13836 (diff) | |
discriminate: Do fresh_global in the right env in presence of side-effects.
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 53678aa848..c442178c10 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -901,7 +901,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = let i = build_coq_I () in let absurd_term = build_coq_False () in let eq_elim, eff = ind_scheme_of_eq lbeq in - let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in + let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), eff |