diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 95cfd73a0..a23b1b64a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -53,7 +53,7 @@ let rec under_binders env f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole (loc, k, _) -> + | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", |