diff options
| author | Hugo Herbelin | 2019-11-14 12:44:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:41 +0100 |
| commit | 32467acf285629c28cbda27d27a8cf248150f2bc (patch) | |
| tree | 382cac5f44d43143116b864e082bc63a5a7d11a0 /interp/constrextern.ml | |
| parent | 3eea1e383e23ea76fcd49a7b302f31b2e3f6ef2a (diff) | |
Fix index bug in computing implicit signature of abbrev. in pattern printing.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 008e84cd9c..b05ca8e5a6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -537,7 +537,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else - match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in |