diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 15:57:27 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 19:14:19 -0400 |
| commit | aa63497700bb2e75767c1891a961fc06ba329065 (patch) | |
| tree | 3ddd6a1060fe1d134d13a087d90a26400a39ce45 /checker/reduction.mli | |
| parent | 283ce711d67d18889e0e4acf51d9ef15a35e6ab7 (diff) | |
Porting guard fix to checker.
Diffstat (limited to 'checker/reduction.mli')
| -rw-r--r-- | checker/reduction.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/reduction.mli b/checker/reduction.mli index 915805d26..4b64f9af7 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -47,5 +47,7 @@ val hnf_prod_applist : env -> constr -> constr list -> constr val dest_prod : env -> constr -> rel_context * constr val dest_prod_assum : env -> constr -> rel_context * constr +val dest_lam_assum : env -> constr -> rel_context * constr + val dest_arity : env -> constr -> arity |