diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 18:18:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 19:03:38 +0100 |
| commit | f02f64a21863ce03f2da4ff04cd003051f96801f (patch) | |
| tree | 601fded539120c931b4ece1cff9d0790bdd82fea /tactics/eqschemes.ml | |
| parent | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (diff) | |
Removing some goal unsafeness in inductive schemes.
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b2603315d..76bf13a57 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -58,6 +58,7 @@ open Namegen open Inductiveops open Ind_tables open Indrec +open Sigma.Notations let hid = Id.of_string "H" let xid = Id.of_string "X" @@ -630,9 +631,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (**********************************************************************) let build_r2l_rew_scheme dep env ind k = - let sigma, indu = Evd.fresh_inductive_instance env (Evd.from_env env) ind in - let sigma', c = build_case_analysis_scheme env sigma indu dep k in - c, Evd.evar_universe_context sigma' + let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in + let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in + let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in + c, Evd.evar_universe_context (Sigma.to_evar_map sigma) let build_l2r_rew_scheme = build_l2r_rew_scheme let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme |