diff options
Diffstat (limited to 'contrib/funind/invfun.ml')
| -rw-r--r-- | contrib/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 0160c290f..63d44916b 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -573,9 +573,9 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (pf_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 - then Equality.discr id g + then Equality.discrHyp id g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g + then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) |