diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4a5f4e5c820f..a6b8283be07c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1218,12 +1218,6 @@ plugin:ci-paramcoq: - build:edge+flambda - library:ci-stdlib+flambda -plugin:ci-perennial: - extends: .ci-template-flambda - needs: - - build:edge+flambda - - library:ci-stdlib+flambda - plugin:plugin-tutorial: stage: build-0 interruptible: true diff --git a/Makefile.ci b/Makefile.ci index 8cc4d67c17ce..2054b582e441 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -89,7 +89,6 @@ CI_TARGETS= \ ci-oddorder \ ci-paco \ ci-parsec \ - ci-perennial \ ci-quickchick_test \ ci-refman \ ci-rewriter \ @@ -231,8 +230,6 @@ ci-compcert: ci-menhir ci-flocq ci-paramcoq: ci-stdlib -ci-perennial: ci-stdlib - ci-aac_tactics: ci-stdlib ci-relation_algebra: ci-aac_tactics ci-mathcomp diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 31b0d1534e14..3adc0d8a501b 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -120,8 +120,7 @@ project corn "https://github.com/coq-community/corn" "master" # NB: stdpp and Iris refs are gotten from the opam files in the Iris and # iris_examples repos respectively. So just getting a fix landed in stdpp or # Iris is not enough. Ping @RalfJung and @robbertkrebbers if you need the -# versions of stdpp or Iris to be bumped. Perennial also has its own pinned -# versions of stdpp and Iris; ping @tchajed and @zeldovich to get that bumped. +# versions of stdpp or Iris to be bumped. project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" "" # Contact @RalfJung, @robbertkrebbers on github @@ -437,16 +436,6 @@ project argosy "https://github.com/mit-pdos/argosy" "master" project atbr "https://github.com/coq-community/atbr" "master" # Contact @palmskog, @tchajed on github -######################################################################## -# perennial -######################################################################## -project perennial "https://github.com/mit-pdos/perennial" "coq/tested" -# Contact @upamanyus, @tchajed on github -# PRs to fix Perennial failures should be submitted against the Perennial -# `master` branch. `coq/tested` is automatically updated every night to the -# `master` branch if CI on `master` is green. This is to avoid breaking Coq CI -# when Perennial CI breaks. - ######################################################################## # metarocq ######################################################################## diff --git a/dev/ci/scripts/ci-perennial.sh b/dev/ci/scripts/ci-perennial.sh deleted file mode 100644 index c24c907b5ad1..000000000000 --- a/dev/ci/scripts/ci-perennial.sh +++ /dev/null @@ -1,18 +0,0 @@ -#!/usr/bin/env bash - -set -e - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -WITH_SUBMODULES=1 -git_download perennial - -if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi - -ulimit -s -ulimit -s 65536 -ulimit -s -( cd "${CI_BUILD_DIR}/perennial" - make TIMED=false lite -) diff --git a/dev/ci/user-overlays/21609-proux01-if-is.sh b/dev/ci/user-overlays/21609-proux01-if-is.sh new file mode 100644 index 000000000000..ddb7fce815bd --- /dev/null +++ b/dev/ci/user-overlays/21609-proux01-if-is.sh @@ -0,0 +1,3 @@ +overlay bedrock2 https://github.com/proux01/bedrock2 rocq21478 21609 +overlay itree https://github.com/proux01/InteractionTrees rocq21478 21609 +overlay unimath https://github.com/proux01/UniMath rocq21478 21609 diff --git a/doc/changelog/02-specification-language/21611-if-is.rst b/doc/changelog/02-specification-language/21611-if-is.rst new file mode 100644 index 000000000000..a9006d704691 --- /dev/null +++ b/doc/changelog/02-specification-language/21611-if-is.rst @@ -0,0 +1,7 @@ +- **Added:** + new syntactic sugar `if g is c then t else e` + and `if g isn't c then t else e` for `match g with c => t | _ => e end` + and `match g with c => e | _ => t end` respectively. This adds the + new reserved keywords `is` and `isn't` + (`#21478 `_, + by Pierre Roux). diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9500325363e9..843d22615fcb 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -189,7 +189,7 @@ Keywords _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop SProp Set Theorem Type Variable as at cofix else end - fix for forall fun if in let match return then where with + fix for forall fun if in is isn't let match return then where with The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index ee61d9235dfb..4224ae8b0bee 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -34,10 +34,14 @@ is often not successful and prints the expanded form. Pattern-matching on boolean values: the if expression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. insertprodn term_if term_if +.. insertprodn term_if if_else .. prodn:: term_if ::= if @term {? {? as @name } return @term100 } then @term else @term + | if @term is @if_dthen @if_else + | if @term isn't @if_dthen @if_else + if_dthen ::= @pattern {? in @pattern } {? return @term100 } then @term + if_else ::= else @term For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible @@ -77,6 +81,10 @@ and :n:`@ident__2`, the following terms are equal: Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is declared as such (see :ref:`controlling-match-pp`). +The `if g is c then t else e` and `if g isn't c then t else e` +syntaxes are syntactic sugar for `match g with c => t | _ => e end` +and `match g with c => e | _ => t end` respectively. + .. _irrefutable-patterns: Irrefutable patterns: the destructuring let variants diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 2b12707243fe..fbff137c8568 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -264,6 +264,8 @@ binder_constr: [ | MOVETO term_forall_or_fun "fun" open_binders "=>" term200 | MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200 | MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200 +| MOVETO term_if "if" term200 "is" if_dthen if_else +| MOVETO term_if "if" term200 "isn't" if_dthen if_else | MOVETO term_fix "let" "fix" fix_decl "in" term200 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ffd5402734a2..3b0a141bb3fa 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -163,10 +163,20 @@ binder_constr: [ | "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 | "let" "'" pattern200 OPT [ "in" pattern200 ] ":=" term200 OPT case_type "in" term200 | "if" term200 as_return_type "then" term200 "else" term200 +| "if" term200 "is" if_dthen if_else +| "if" term200 "isn't" if_dthen if_else | "fix" fix_decls | "cofix" cofix_decls ] +if_dthen: [ +| pattern200 OPT [ "in" pattern200 ] OPT case_type "then" lconstr +] + +if_else: [ +| "else" lconstr +] + arg: [ | test_lpar_id_coloneq "(" identref ":=" lconstr ")" | test_lpar_nat_coloneq "(" natural ":=" lconstr ")" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d3cd93739132..12b6a7673106 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -369,6 +369,16 @@ cofix_body: [ term_if: [ | "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term +| "if" term "is" if_dthen if_else +| "if" term "isn't" if_dthen if_else +] + +if_dthen: [ +| pattern OPT [ "in" pattern ] OPT ( "return" term100 ) "then" term +] + +if_else: [ +| "else" term ] term_let: [ diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 6c32c6c54dd1..0e8d75c4d428 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -303,9 +303,25 @@ GRAMMAR EXTEND Gram "then"; b1 = term LEVEL "200"; "else"; b2 = term LEVEL "200" -> { CAst.make ~loc @@ CIf (c, po, b1, b2) } + | "if"; c = term LEVEL "200"; "is"; db1 = if_dthen; b2 = if_else -> + { let b1, (na, t), rt = db1 in + CAst.make ~loc @@ CCases (MatchStyle, rt, [c, na, t], [b1; b2]) } + | "if"; c = term LEVEL "200"; "isn't"; db1 = if_dthen; b2 = if_else -> + { let b1, (na, t), rt = db1 in + let b1, b2 = let open CAst in + let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in + (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) in + CAst.make ~loc @@ CCases (MatchStyle, rt, [c, na, t], [b1; b2]) } | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) } | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; + if_dthen: + [ [ mp = pattern; t = OPT ["in"; t = pattern -> { t } ]; rt = OPT case_type; "then"; c = lconstr -> + { let ct = match t, rt with None, None -> None | _ -> aliasvar mp in + (CAst.make ~loc ([[mp]], c)), (ct, t), rt } ]]; + if_else: + [ [ mp = [ "else" -> { CAst.make ~loc @@ CPatAtom None } ]; c = lconstr -> + { CAst.make ~loc ([[mp]], c) } ]]; arg: [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } | test_lpar_nat_coloneq; "("; n = natural; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByPos n)) } diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 1df591df336e..ccf3fa7792a2 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -44,17 +44,15 @@ IGNORE KEYWORDS (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. *)(* ************) +(** Alternative notations for anonymous arguments. *)(* ************) (* Syntax: *) -(* if is then ... else ... *) -(* if is [in ..] return ... then ... else ... *) (* let: := in ... *) (* let: [in ...] := return ... in ... *) (* The scope of a top-level 'as' in the pattern extends over the *) -(* 'return' type (dependent if/let). *) +(* 'return' type (dependent let). *) (* Note that the optional "in ..." appears next to the *) -(* rather than the in then "let:" syntax. The alternative *) +(* rather than the in the "let:" syntax. The alternative *) (* would lead to ambiguities in, e.g., *) (* let: p1 := (*v---INNER LET:---v *) *) (* let: p2 := let: p3 := e3 in k return t in k2 in k1 return t' *) @@ -65,9 +63,6 @@ IGNORE KEYWORDS (* display style -- why aren't these strings?); also, the v8.1 *) (* pretty-printer only allows extension hooks for printing *) (* integer or string literals. *) -(* Also note that in the v8 grammar "is" needs to be a keyword; *) -(* as this can't be done from an ML extension file, the new *) -(* syntax will only work when ssreflect.v is imported. *) let no_ct = None, None and no_rt = None let aliasvar = function @@ -76,7 +71,6 @@ let aliasvar = function let mk_cnotype mp = aliasvar mp, None let mk_ctype mp t = aliasvar mp, Some t let mk_rtype t = Some t -let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt let mk_let ?loc rt ct mp c1 = CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) let mk_pat c (na, t) = (c, na, t) @@ -87,25 +81,8 @@ GRAMMAR EXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; - ssr_dpat: [ - [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } - | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt } - | mp = ssr_mpat -> { mp, no_ct, no_rt } - ] ]; - ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]]; - ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: TOP [ - [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> - { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> - { let b1, ct, rt = db1 in - let b1, b2 = let open CAst in - let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in - (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) - in - CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> + [ "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 } | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> diff --git a/test-suite/bugs/bug_16975.v b/test-suite/bugs/bug_16975.v index 04c9717c9199..d8672927dcbf 100644 --- a/test-suite/bugs/bug_16975.v +++ b/test-suite/bugs/bug_16975.v @@ -43,8 +43,8 @@ Notation "X ≃ Y" := (weq X%type Y%type) : type_scope. Definition pr1weq {X Y : Type} := pr1 : X ≃ Y -> (X -> Y). Coercion pr1weq : weq >-> Funclass. -Definition make_weq {X Y : Type} (f : X -> Y) (is: isweq f) : X ≃ Y. -exact (tpair (λ f : X -> Y, isweq f) f is). +Definition make_weq {X Y : Type} (f : X -> Y) (isf: isweq f) : X ≃ Y. +exact (tpair (λ f : X -> Y, isweq f) f isf). Defined. Theorem twooutof3c {X Y Z : Type} (f : X -> Y) (g : Y -> Z) diff --git a/test-suite/bugs/bug_3374.v b/test-suite/bugs/bug_3374.v index d8e72f4f2042..2142991e3109 100644 --- a/test-suite/bugs/bug_3374.v +++ b/test-suite/bugs/bug_3374.v @@ -24,7 +24,7 @@ Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) := forall x x' x0 x0' : X , R x x' -> R x0 x0' -> paths ( f x x0 ) ( f x' x0' ) . Axiom setquotuniv : forall { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y . -Definition setquotuniv2 { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) +Definition setquotuniv2 { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( isf : iscomprelfun2 R f ) ( c c0 : setquot R ) : Y . Proof. intros . diff --git a/test-suite/bugs/bug_3375.v b/test-suite/bugs/bug_3375.v index 1e0c8e61f4d4..20b947dab867 100644 --- a/test-suite/bugs/bug_3375.v +++ b/test-suite/bugs/bug_3375.v @@ -8,7 +8,7 @@ Definition UU := Set. Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . Definition hProp := sigT (fun X : Type => admit). -Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp. +Axiom hProppair : forall ( X : UU ) ( _ : admit ), hProp. Definition hProptoType := @projT1 _ _ : hProp -> Type . Coercion hProptoType: hProp >-> Sortclass. Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ). diff --git a/test-suite/bugs/bug_6661.v b/test-suite/bugs/bug_6661.v index 1b0396e5a275..f68f69e5d31d 100644 --- a/test-suite/bugs/bug_6661.v +++ b/test-suite/bugs/bug_6661.v @@ -123,10 +123,10 @@ Defined. Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr. -Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'. +Lemma proofirrelevancecontr {X : UU} (isc : iscontr X) (x x' : X) : x = x'. Proof. intros. - induction is as [y fe]. + induction isc as [y fe]. exact (fe x @ !(fe x')). Defined. @@ -214,10 +214,10 @@ Section isweqcontrtounit. (* Constraint uu0 < i. *) (* Without this constraint, we get i = uu0 in the next definition *) - Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt). + Lemma isweqcontrtounit@{} {T : Type@{i}} (isc : iscontr@{i} T) : isweq@{i} (λ _:T, tt). Proof. intros. intro y. induction y. - induction is as [c h]. + induction isc as [c h]. split with (hfiberpair@{i i i} _ c (idpath tt)). intros ha. induction ha as [x e]. diff --git a/test-suite/output/PrintGrammar.out b/test-suite/output/PrintGrammar.out index 6ac58ee6b468..62163d650fa6 100644 --- a/test-suite/output/PrintGrammar.out +++ b/test-suite/output/PrintGrammar.out @@ -19,6 +19,8 @@ Entry binder_constr is LEVEL "200" | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":="; term LEVEL "200"; "in"; term LEVEL "200" + | "if"; term LEVEL "200"; "is"; if_dthen; if_else + | "if"; term LEVEL "200"; "isn't"; if_dthen; if_else | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else"; term LEVEL "200" | "fix"; fix_decls diff --git a/test-suite/output/PrintGrammarConstr.out b/test-suite/output/PrintGrammarConstr.out index 9b230f711812..e3e7eee7eb74 100644 --- a/test-suite/output/PrintGrammarConstr.out +++ b/test-suite/output/PrintGrammarConstr.out @@ -10,6 +10,8 @@ Entry binder_constr is LEVEL "200" | "let"; [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":="; term LEVEL "200"; "in"; term LEVEL "200" + | "if"; term LEVEL "200"; "is"; if_dthen; if_else + | "if"; term LEVEL "200"; "isn't"; if_dthen; if_else | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else"; term LEVEL "200" | "fix"; fix_decls diff --git a/test-suite/output/PrintKeywords.out b/test-suite/output/PrintKeywords.out index f25f491e162f..02f1fc0bdd97 100644 --- a/test-suite/output/PrintKeywords.out +++ b/test-suite/output/PrintKeywords.out @@ -81,6 +81,8 @@ forall fun if in +is +isn't let match return diff --git a/test-suite/output/PrintNotation.out b/test-suite/output/PrintNotation.out index 7b0eb01c8495..6d0f0970e9f5 100644 --- a/test-suite/output/PrintNotation.out +++ b/test-suite/output/PrintNotation.out @@ -166,9 +166,9 @@ Notation "{ ' _ : _ & _ }" at level 0 with arguments strict pattern at level 0, constr, constr, no associativity. Notation "{ ' _ : _ & _ & _ }" at level 0 with arguments strict pattern at level 0, constr, constr, constr, no associativity. -Notation "if _ is _ then _ else _" at level 200 with arguments constr, -pattern at level 100 at level 100, constr, constr at next level, -no associativity. +Notation "if _ is _ then _ else _" at level 200 with arguments constr +at level 200, pattern at level 100 at level 100, constr at level 200, constr +at level 200, no associativity. Notation "_ -> _" at level 99 with arguments constr at next level, constr at level 200, no associativity. Notation "_ <-> _" at level 95 with arguments constr at next level, constr @@ -263,9 +263,9 @@ Notation "{ ' _ : _ & _ }" at level 0 with arguments strict pattern at level 0, constr, constr, no associativity. Notation "{ ' _ : _ & _ & _ }" at level 0 with arguments strict pattern at level 0, constr, constr, constr, no associativity. -Notation "if _ is _ then _ else _" at level 200 with arguments constr, -pattern at level 100 at level 100, constr, constr at next level, -no associativity. +Notation "if _ is _ then _ else _" at level 200 with arguments constr +at level 200, pattern at level 100 at level 100, constr at level 200, constr +at level 200, no associativity. Notation "{{ _ }}" in Foo at level 0 with arguments custom Foo, no associativity. Notation "{{ _ }}" in Foo at level 0 with arguments custom Foo, diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 8d3bdd521b25..550560794c6f 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -202,12 +202,12 @@ Abort. (* Utilisation de let rec sans arguments *) -Ltac is := +Ltac rec_intros := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. Goal True -> True -> True. -is. +rec_intros. exact I. Abort. diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v index 9035e93a245b..2958b4a97d2c 100644 --- a/test-suite/success/telescope_canonical.v +++ b/test-suite/success/telescope_canonical.v @@ -1,9 +1,9 @@ -Structure Inner := mkI { is :> Type }. +Structure Inner := mkI { ins :> Type }. Structure Outer := mkO { os :> Inner }. Canonical Structure natInner := mkI nat. Canonical Structure natOuter := mkO natInner. Definition hidden_nat := nat. -Axiom P : forall S : Outer, is (os S) -> Prop. +Axiom P : forall S : Outer, ins (os S) -> Prop. Lemma test1 (n : hidden_nat) : P _ n. Admitted. diff --git a/theories/Corelib/Init/Notations.v b/theories/Corelib/Init/Notations.v index b97e86a166d5..fe2e3c1c191f 100644 --- a/theories/Corelib/Init/Notations.v +++ b/theories/Corelib/Init/Notations.v @@ -112,7 +112,7 @@ Module IfNotations. Notation "'if' c 'is' p 'then' u 'else' v" := (match c with p => u | _ => v end) - (at level 200, p pattern at level 100). + (at level 200, c, u, v at level 200, p pattern at level 100). End IfNotations.