diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b946911e0..8b9319a29 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -77,7 +77,7 @@ let rec execute mf env sigma cstr = | IsSort (Type u) -> let (j,_) = judge_of_type u in j - | IsAppL (f,args) -> + | IsApp (f,args) -> let j = execute mf env sigma f in let jl = execute_list mf env sigma (Array.to_list args) in let (j,_) = apply_rel_list env sigma mf.nocheck jl j in |