diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_class.mlg | 8 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 3 |
2 files changed, 7 insertions, 4 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8d197e6056..a86045b0a4 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth @@ -87,11 +87,13 @@ END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - { typeclasses_eauto ~strategy:Bfs ~depth:d l } + { typeclasses_eauto ~depth:d ~strategy:Bfs l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } + typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5dedae6388..cdd15acb0d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -204,7 +204,8 @@ exception NoProgress (* comparison can be much faster than the HO one. *) let unif_EQ env sigma p c = - let evars = existential_opt_value0 sigma, Evd.universes sigma in + let env = Environ.set_universes (Evd.universes sigma) env in + let evars = existential_opt_value0 sigma in try let _ = Reduction.conv env p ~evars c in true with _ -> false let unif_EQ_args env sigma pa a = |