diff options
Diffstat (limited to 'test-suite/bugs/closed/1844.v')
| -rw-r--r-- | test-suite/bugs/closed/1844.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v index 17eeb352..c41e4590 100644 --- a/test-suite/bugs/closed/1844.v +++ b/test-suite/bugs/closed/1844.v @@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. -Implicit Arguments update [A]. +Arguments update [A]. Definition ident := Z. Parameter operator: Set. |