diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/wcclausenv.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e7673944e..8a8025f12 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1597,7 +1597,9 @@ let elim_scheme_type elim t gl = let clause = mk_clenv_type_of wc elim in match kind_of_term (last_arg (clenv_template clause).rebus) with | IsMeta mv -> - let clause' = clenv_unify (clenv_instance_type clause mv) t clause in + let clause' = + (* t is inductive, then CUMUL or CONV is irrelevant *) + clenv_unify CUMUL t (clenv_instance_type clause mv) clause in elim_res_pf kONT clause' gl | _ -> anomaly "elim_scheme_type" diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 63504956c..2c791f3bb 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -93,7 +93,7 @@ let clenv_constrain_with_bindings bl clause = let sigma = Evd.empty in let k_typ = nf_betaiota (clenv_instance_type clause k) in let c_typ = nf_betaiota (w_type_of clause.hook c) in - matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t + matchrec (clenv_assign k c (clenv_unify CUMUL c_typ k_typ clause)) t in matchrec clause bl |