diff options
author | 2016-06-27 20:47:43 +0200 | |
---|---|---|
committer | 2016-06-27 20:47:43 +0200 | |
commit | 663a8647bbc32e11243091de80f9953ed5fb7eff (patch) | |
tree | 7fba0a308daee7586221f752e233dd8fa9c8f5f5 /tactics/auto.ml | |
parent | d4725f692a5f202ca4c5d6341b586b0e377f6973 (diff) | |
parent | a7ea32fbf3829d1ce39ce9cc24b71791727090c5 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r-- | tactics/auto.ml | 22 |
1 files changed, 6 insertions, 16 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e57b48e9e..6c1f38d48 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -94,7 +94,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c - + let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in @@ -109,21 +109,11 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - let (c, _, _) = c in - let ctx, c' = - if poly then - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let ctx = Evd.evar_universe_context evd' in - ctx, subst_univs_level_constr subst c - else - let ctx = Evd.evar_universe_context clenv.evd in - ctx, c - in - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in - let sigma = Evd.merge_universe_context sigma ctx in - Sigma.Unsafe.of_pair (exact_check c', sigma) + Proofview.Goal.enter { enter = begin fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (exact_check c) end } (* Util *) |