diff options
| author | Matthieu Sozeau | 2014-06-26 11:05:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-26 11:05:00 +0200 |
| commit | 83ae5e6ad95372912ba9eb9f8c52d857cdf10021 (patch) | |
| tree | 6698ac68f45940456cafb56aaaf0dec36bfb408f /test-suite/bugs/closed/2966.v | |
| parent | f6382ef326099651cd051aa907b4e9ac6c905698 (diff) | |
Change interface of refresh universes to get a pbty argument instead of
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
Diffstat (limited to 'test-suite/bugs/closed/2966.v')
| -rw-r--r-- | test-suite/bugs/closed/2966.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v index e1c8d00474..debada8539 100644 --- a/test-suite/bugs/closed/2966.v +++ b/test-suite/bugs/closed/2966.v @@ -7,7 +7,7 @@ Set Asymmetric Patterns. Module MemSig. Definition t: Type := list Type. - Definition Nth (sig: t) (n: nat): Type := + Definition Nth (sig: t) (n: nat) := nth n sig unit. End MemSig. |