diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-25 17:47:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-25 17:48:30 +0100 |
| commit | 765c6b15b76fd407a4d888d3f5e8cc532901045b (patch) | |
| tree | f9f003d053ffbf0e6cfa2f660d5b74441b551aaa /checker/inductive.ml | |
| parent | c695e5adb3cb5492d412d933b1dd7901dc6676af (diff) | |
[checker] Remove duplicated function
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 22353ec16..fb33cd96b 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -435,12 +435,6 @@ type subterm_spec = | Dead_code | Not_subterm -let eq_recarg r1 r2 = match r1, r2 with -| Norec, Norec -> true -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false - let eq_wf_paths = Rtree.equal eq_recarg let inter_recarg r1 r2 = match r1, r2 with |