diff options
| author | Matthieu Sozeau | 2014-06-18 17:16:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-18 17:21:21 +0200 |
| commit | 23f4804b50307766219392229757e75da9aa41d9 (patch) | |
| tree | 4df833759b600b1a3d638bdbc65cf5060eb3e24f /test-suite | |
| parent | 77839ae306380e99a8ceac0bf26ff86ec9159346 (diff) | |
Proofs now take and return an evar_universe_context, simplifying interfaces
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_062.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v index e0ff5459cf..7f1908f081 100644 --- a/test-suite/bugs/opened/HoTT_coq_062.v +++ b/test-suite/bugs/opened/HoTT_coq_062.v @@ -65,16 +65,17 @@ Definition e : Bool <~> Bool. admit. Defined. -Definition p `{Univalence} : Bool = Bool := path_universe e. +Definition p `{Univalence} : @paths Set Bool Bool := path_universe e. Theorem thm `{Univalence} : (forall A : Set, ((A -> False) -> False) -> A) -> False. intro f. Set Printing Universes. Set Printing All. + pose proof (apD f p). + pose(path_universe e). pose proof (apD f (path_universe e)). - cut `{Univalence}; intros. pose proof (apD f p). -Admitted. - (* ??? Toplevel input, characters 0-37: + admit. +Defined. (* ??? Toplevel input, characters 0-37: Error: Unable to satisfy the following constraints: In environment: |