diff options
| author | SimonBoulier | 2019-12-02 12:52:39 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-02-04 16:07:21 +0100 |
| commit | a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 (patch) | |
| tree | 536f901c47c0080a5bc6a2d3b92adaefbfc8490f /interp/implicit_quantifiers.ml | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8b457ab37b..ffbb982ab7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -203,8 +203,9 @@ let warn_ignoring_implicit_status = let implicits_of_glob_constr ?(with_products=true) l = let add_impl ?loc na bk l = match bk with - | Implicit -> CAst.make ?loc (Some (na,true)) :: l - | _ -> CAst.make ?loc None :: l + | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l + | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l + | Explicit -> CAst.make ?loc None :: l in let rec aux c = match DAst.get c with @@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then add_impl na bk (aux b) else let () = match bk with - | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc - | _ -> () + | NonMaxImplicit + | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | Explicit -> () in [] | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) | GLetIn (na, b, t, c) -> aux c |