diff options
| author | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
| commit | e76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (patch) | |
| tree | 5bcdbed2dac27feeb27caf840e8cad24e7483a9a /interp/constrintern.ml | |
| parent | aff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff) | |
| parent | 0dac9618c695a345f82ee302b205217fff29be29 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 982d9bfe39..8c56d0ccfe 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for = let (argscs,_) = find_remaining_scopes pats [] g in Some (g, List.map2 (in_pat_sc env) argscs pats, []) | NApp (NRef g,args) -> - ensure_kind top loc g; + test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; let pats1,pats2 = List.chop nvars pats in |