diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-09 22:39:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-09 22:53:59 +0200 |
| commit | 0dd3f0d34873dcd126be8ec48724a310214f38ac (patch) | |
| tree | ccb5c83cba1db777681e8ecb7251dc486b3f2044 /library/impargs.ml | |
| parent | e365fb8ffbbc62352a725de13cbf864b3fbb3840 (diff) | |
- Fix printing and parsing of primitive projections, including the Set
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 55e21b2c8..355cbe1fa 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -378,7 +378,9 @@ let set_manual_implicits env flags enriching autoimps l = l, imp, m in let imps' = merge (k+1) l' imps in - let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in + let m = Option.map (fun (b,f) -> + (* match imp with Some Manual -> (b,f) *) + (* | _ -> *)set_maximality imps' b, f) m in Option.map (set_implicit id imp) m :: imps' | (Anonymous,imp)::imps -> let l', forced = try_forced k l in |