diff options
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5c3e73e9d..5ef8f05bb 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed |