diff options
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index d54bbee4e3..4eb05df74d 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -484,7 +484,7 @@ let check_and_adjust_constructor env ind cstrs = function | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if Closure.mind_equiv env ind' ind then + if Names.eq_ind ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 76a8a03221..f617c1008d 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -155,7 +155,7 @@ let cache (_, (infos, tac)) = let load (_, (_, tac)) = set_default_tactic tac -let subst (_, s, (infos, tac)) = +let subst (s, (infos, tac)) = (infos, Tacinterp.subst_tactic s tac) let (input,output) = |