diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /test-suite/misc | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'test-suite/misc')
| -rw-r--r-- | test-suite/misc/quotation_token/src/quotation.mlg | 2 | ||||
| -rw-r--r-- | test-suite/misc/side-eff-leak-univs/src/evil.mlg | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index ba0bcb1b3c..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index d89ab887a8..bb6eaff409 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -7,7 +7,7 @@ open Stdarg TACTIC EXTEND magic | [ "magic" ident(i) ident(j) ] -> { - let open Glob_term in - DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() + let open Constrexpr in + DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() } END |