diff options
| author | Pierre-Marie Pédrot | 2015-11-05 16:34:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-05 16:34:37 +0100 |
| commit | 55a765faa95d7be9a1e4c37096139f57f288f55a (patch) | |
| tree | 459ac71b1478d69f77f8663c1001c10ca0ae528d /engine/evd.ml | |
| parent | 35afb42a6bb30634d2eb77a32002ed473633b5f4 (diff) | |
| parent | 0fd6ad21121c7c179375b9a50c3135abab1781b2 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 40409fe7fd..60239ebfe2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -945,7 +945,7 @@ let update_sigma_env evd env = (* Conversion w.r.t. an evar map and its local universes. *) -let conversion_gen env evd pb t u = +let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> Reduction.trans_conv_universes @@ -955,14 +955,8 @@ let conversion_gen env evd pb t u = full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u -(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) -(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) - -let conversion env d pb t u = - conversion_gen env d pb t u; d - let test_conversion env d pb t u = - try conversion_gen env d pb t u; true + try test_conversion_gen env d pb t u; true with _ -> false exception UniversesDiffer = UState.UniversesDiffer |