diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 14:20:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 15:26:51 +0100 |
| commit | 96f8d358c7d3c9a08ff2006f42716bc64937dad2 (patch) | |
| tree | c7a6503e6b39681aee60e556827614b5b3512778 /tactics/elim.ml | |
| parent | 49a764bd81ac1b21130d54a1808ce95b9992a36d (diff) | |
Fixing pervasive equalities. In particular, I removed the code that deleted
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 81fab6e2b..06f84ecd1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -107,7 +107,7 @@ let head_in indl t gl = if !up_to_delta then find_mrectype env sigma t else extract_mrectype t - in List.mem ity indl + in List.exists (fun i -> eq_ind i ity) indl with Not_found -> false let decompose_these c l = |