diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /checker/inductive.ml | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index ae2f7de8a..8f23a38af 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with let eq_wf_paths = Rtree.equal eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 |