type id = string;;
type joint_recursion_kind =
- [ `Recursive
+ [ `Recursive of int list (* decreasing arguments *)
| `CoRecursive
| `Inductive of int (* paramsno *)
| `CoInductive of int (* paramsno *)
}
and 'term arg =
- Aux of int
+ Aux of string
| Premise of premise
| Term of 'term
| ArgProof of 'term proof