diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bd5fc9890774..758c840dc871 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1229,12 +1229,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 70708e47a530..62f7587c51f5 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -164,8 +164,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 b97e041df281..872c13362425 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -123,8 +123,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
 
@@ -440,16 +439,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/22124-proux01-if-printing.sh b/dev/ci/user-overlays/22124-proux01-if-printing.sh
new file mode 100644
index 000000000000..2933f5a372d7
--- /dev/null
+++ b/dev/ci/user-overlays/22124-proux01-if-printing.sh
@@ -0,0 +1,2 @@
+overlay hott https://github.com/proux01/HoTT rocq22124 22124
+overlay mtac2 https://github.com/proux01/Mtac2 rocq22124 22124
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..9e3a1ff02396
--- /dev/null
+++ b/doc/changelog/02-specification-language/21611-if-is.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  new syntactic sugar `if g is c then t else e`
+  for `match g with c => t | _ => e end`. This adds the
+  new reserved keyword `is`
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  by Pierre Roux).
diff --git a/doc/changelog/02-specification-language/22124-if-printing-Removed.rst b/doc/changelog/02-specification-language/22124-if-printing-Removed.rst
new file mode 100644
index 000000000000..be8b43a4ead1
--- /dev/null
+++ b/doc/changelog/02-specification-language/22124-if-printing-Removed.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  table ``Printing If``
+  (`#22124 <https://github.com/rocq-prover/rocq/pull/22124>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index f0a5a7666947..f83c90f857a2 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 of return then where with
+    fix for forall fun if in is let match of 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 8269a5b1d6b6..e5637b05e9d6 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -34,10 +34,13 @@ 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_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 +80,9 @@ 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` syntax is syntactic sugar for `match g
+with c => t | _ => e end`.
+
 .. _irrefutable-patterns:
 
 Irrefutable patterns: the destructuring let variants
@@ -313,19 +319,6 @@ written using the :ref:`let-tuple syntax <let-tuple>`.
    Use the :cmd:`Add` and :cmd:`Remove` commands to update this set.
 
 
-Printing matching on booleans
-+++++++++++++++++++++++++++++
-
-If an inductive type is isomorphic to the boolean type, pattern matching
-can be written using ``if`` … ``then`` … ``else`` ….  This table controls
-which types are written this way:
-
-.. table:: Printing If @qualid
-
-   This :term:`table` specifies a set of qualids for which pattern matching is displayed using
-   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add` and :cmd:`Remove`
-   commands to update this set.
-
 This example emphasizes what the printing settings offer.
 
 .. example::
@@ -355,7 +348,7 @@ Printing regular match syntax
 
    When enabled, this flag makes printing avoid the alternate case
    analysis syntaxes (with :ref:`if <if-then-else>` and :ref:`let
-   <irrefutable-patterns>`), overriding :table:`Printing If` and
+   <irrefutable-patterns>`), overriding
    :table:`Printing Let` and disregarding the syntax used to input the
    case analysis (so e.g. `let 'tt := tt in tt` will be printed using `match`).
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 8ab6b9c2165e..577d5c5a1371 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -264,6 +264,7 @@ term10: [
 | 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_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 dd4fdea97af4..4ce7c336a559 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -109,6 +109,7 @@ term10: [
 | "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
 | "fix" fix_decls
 | "cofix" cofix_decls
 | term9
@@ -145,6 +146,14 @@ term0: [
 | "ltac" ":" "(" Pltac.ltac_expr ")"
 ]
 
+if_dthen: [
+| pattern200 OPT [ "in" pattern200 ] OPT case_type "then" lconstr
+]
+
+if_else: [
+| "else" lconstr
+]
+
 array_elems: [
 | LIST0 lconstr SEP ";"
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index bf3fca66453f..65f91bf278e0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -369,6 +369,15 @@ cofix_body: [
 
 term_if: [
 | "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+| "if" term "is" if_dthen if_else
+]
+
+if_dthen: [
+| pattern OPT [ "in" pattern ] OPT ( "return" term100 ) "then" term
+]
+
+if_else: [
+| "else" term
 ]
 
 term_let: [
diff --git a/ide/rocqide/rocq_commands.ml b/ide/rocqide/rocq_commands.ml
index 296fb20eea73..c7bba9098204 100644
--- a/ide/rocqide/rocq_commands.ml
+++ b/ide/rocqide/rocq_commands.ml
@@ -15,7 +15,6 @@ let commands = [
    "Add Field";
    "Add Morphism";
    "Add Printing Constructor";
-   "Add Printing If";
    "Add Printing Let";
    "Add Printing Record";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
@@ -94,7 +93,6 @@ let commands = [
    "Record";
    "Remark";
    "Remove Printing Constructor";
-   "Remove Printing If";
    "Remove Printing Let";
    "Remove Printing Record";
    "Require";
@@ -128,7 +126,6 @@ let commands = [
      "Syntactic Definition";
      "Syntax";];
   [
-   "Test Printing If";
    "Test Printing Let";
    "Test Printing Synth";
    "Test Printing Wildcard";
@@ -194,7 +191,6 @@ let state_preserving = [
   "Print Scopes.";
   "Print Section";
 
-  "Print Table Printing If.";
   "Print Table Printing Let.";
   "Print Tables.";
   "Print Term";
@@ -219,7 +215,6 @@ let state_preserving = [
   "Show Proof";
   "Show Tree";
 
-  "Test Printing If";
   "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index a461df52e8b5..f31b376dab0a 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -247,6 +247,9 @@ 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 (IfStyle, 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) } ]
     | "9"
@@ -288,6 +291,15 @@ GRAMMAR EXTEND Gram
       | "`("; c = term LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, c) } ] ]
   ;
+  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) } ]]
+  ;
   array_elems:
     [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]]
   ;
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index ccd46159c1d5..a8ebbcb60ac9 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -43,15 +43,15 @@ IGNORE KEYWORDS
 
 (* global syntactic changes and vernacular commands *)
 
-(** Alternative notations for "match" and anonymous arguments. *)(* ************)
+(** Alternative notations for anonymous arguments. *)(* ************)
 
 (* Syntax:                                                        *)
 (*  let: <pattern> := <term> in ...                               *)
 (*  let: <pattern> [in ...] := <term> 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 <pattern>  *)
-(* rather than the <term> in then "let:" syntax. The alternative  *)
+(* rather than the <term> 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' *)
@@ -62,9 +62,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
diff --git a/plugins/ssrrewrite/ssrrewrite.mlg b/plugins/ssrrewrite/ssrrewrite.mlg
index c50cf3fe7dfd..aad13c565cf5 100644
--- a/plugins/ssrrewrite/ssrrewrite.mlg
+++ b/plugins/ssrrewrite/ssrrewrite.mlg
@@ -127,9 +127,7 @@ GRAMMAR EXTEND Gram
   ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
   ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
   term: LEVEL "10" [
-    [ "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 ->
+    [ "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
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cca1f9881327..b1f2b458f6e1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -222,20 +222,10 @@ let encode_inductive env r =
 
 (* Parameterization of the translation from constr to ast      *)
 
-(* Tables for Cases printing under a "if" form, a "let" form,  *)
-
-let has_two_constructors lc =
-  Int.equal (Array.length lc) 2 (* & lc.(0) = 0 & lc.(1) = 0 *)
+(* Table for Cases printing under a "let" form,  *)
 
 let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 
-let encode_bool env ({CAst.loc} as r) =
-  let (x,lc) = encode_inductive env r in
-  if not (has_two_constructors lc) then
-    user_err ?loc
-      (str "This type has not exactly two constructors.");
-  x
-
 let encode_tuple env ({CAst.loc} as r) =
   let (x,lc) = encode_inductive env r in
   if not (isomorphic_to_tuple lc) then
@@ -243,18 +233,6 @@ let encode_tuple env ({CAst.loc} as r) =
       (str "This type cannot be seen as a tuple type.");
   x
 
-module PrintingCasesIf =
-  PrintingFlags.PrintingInductiveMake (struct
-    let encode = encode_bool
-    let field = "If"
-    let title = "Types leading to pretty-printing of Cases using a `if' form:"
-    let member_message s b =
-      str "Cases on elements of " ++ s ++
-      str
-        (if b then " are printed using a `if' form"
-         else " are not printed using a `if' form")
-  end)
-
 module PrintingCasesLet =
   PrintingFlags.PrintingInductiveMake (struct
     let encode = encode_tuple
@@ -268,7 +246,6 @@ module PrintingCasesLet =
          else " are not printed using a `let' form")
   end)
 
-module PrintingIf  = Goptions.MakeRefTable(PrintingCasesIf)
 module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
 
 (** univ and sort detyping *)
@@ -616,6 +593,9 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
       n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
+  let ci_bool =
+    match Rocqlib.lib_ref_opt "core.bool.type" with None -> false
+    | Some bool -> GlobRef.CanOrd.equal (IndRef ci.ci_ind) bool in
   let tag =
     let tag = ci.ci_pp_info.style in
     if flags.flg.always_regular_match_style then
@@ -624,7 +604,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
       tag
     else if PrintingLet.active ci.ci_ind then
       LetStyle
-    else if PrintingIf.active ci.ci_ind then
+    else if ci_bool then
       IfStyle
     else
       tag
@@ -641,7 +621,7 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
     let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
     GLetTuple (nal,(alias,pred),tomatch,d)
   | IfStyle, None ->
-      if Array.for_all (fun br -> is_nondep_branch sigma br) bl then
+      if ci_bool && Array.for_all (fun br -> is_nondep_branch sigma br) bl then
         let map i br =
           let ctx, body = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
           EConstr.it_mkLambda_or_LetIn body ctx
@@ -653,7 +633,11 @@ let detype_case ~flags computable detype detype_eqns avoid env sigma (ci, univs,
         GIf (tomatch,(alias,pred), nondepbrs.(0), nondepbrs.(1))
       else
         let eqnl = detype_eqns constructs (ci, univs, params, bl) in
-        GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+        if Array.length bl = 2 && is_nondep_branch sigma bl.(0)
+           && not (is_nondep_branch sigma bl.(1)) then
+          GCases (tag,pred,[tomatch,(alias,aliastyp)],List.rev eqnl)
+        else
+          GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
       let eqnl = detype_eqns constructs (ci, univs, params, bl) in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f286f29b82af..bd4dd711fe1f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -731,6 +731,18 @@ let pr ~flags pr sep lev_after inherited a =
                  pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
                  spc () ++ keyword "in" ++ pr spc lev_after ltop b)))
       lletpattern
+  | CCases(Constr.IfStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b1)};{v=(_,b2)}]) ->
+    return (fun lev_after ->
+        hv 0 (
+          hov 1 (keyword "if" ++ spc () ++ pr mt no_after ltop c
+                 ++ pr_as_in ~flags (pr mt no_after ltop) as_clause in_clause
+                 ++ spc () ++ keyword "is" ++ spc ()
+                 ++ pr_patt ~flags (pr mt no_after ltop) no_after ltop p) ++
+          spc () ++
+          hov 0 (keyword "then"
+                 ++ pr (fun () -> brk (1,1)) no_after ltop b1) ++ spc () ++
+          hov 0 (keyword "else" ++ pr (fun () -> brk (1,1)) lev_after ltop b2)))
+      lif
   | CCases(_,rtntypopt,c,eqns) ->
     return (fun lev_after ->
         v 0
diff --git a/test-suite/bugs/bug_16975.v b/test-suite/bugs/bug_16975.v
index 721223bd4543..edd7c9455e4d 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 359c73c345c7..2f5995d46733 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/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 15933f3d6166..414d07d85a49 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -28,7 +28,7 @@ negb is not universe polymorphic
 Arguments negb b%_bool_scope
 negb is transparent
 Expands to: Constant Corelib.Init.Datatypes.negb
-Declared in library Corelib.Init.Datatypes, line 88, characters 11-15
+Declared in library Corelib.Init.Datatypes, line 86, characters 11-15
 a : bool -> bool
 
 a is not universe polymorphic
@@ -43,7 +43,7 @@ negb is not universe polymorphic
 Arguments negb b
 negb is transparent
 Expands to: Constant Corelib.Init.Datatypes.negb
-Declared in library Corelib.Init.Datatypes, line 88, characters 11-15
+Declared in library Corelib.Init.Datatypes, line 86, characters 11-15
 negb' : bool -> bool
 
 negb' is not universe polymorphic
@@ -68,7 +68,7 @@ negb is not universe polymorphic
 Arguments negb b
 negb is transparent
 Expands to: Constant Corelib.Init.Datatypes.negb
-Declared in library Corelib.Init.Datatypes, line 88, characters 11-15
+Declared in library Corelib.Init.Datatypes, line 86, characters 11-15
 negb' : bool -> bool
 
 negb' is not universe polymorphic
diff --git a/test-suite/output/If.out b/test-suite/output/If.out
new file mode 100644
index 000000000000..a9495133153a
--- /dev/null
+++ b/test-suite/output/If.out
@@ -0,0 +1,50 @@
+if true then 1 else 0
+     : nat
+if 4 is 0 then 1 else 0
+     : nat
+if 4 is S n then n else 0
+     : nat
+if 4 is 0 then 0 else 1
+     : nat
+if 4 is 0 then 1 else 0
+     : nat
+match A with
+| A => 0
+| _ => 1
+end
+     : nat
+if B is C then 1 else 0
+     : nat
+match B return nat with
+| A => O
+| B => O
+| C => S O
+end
+     : nat
+if B is C then 1 else 0
+     : nat
+match B with
+| C => 1
+| _ => 0
+end
+     : nat
+if B is C then 1 else 0
+     : nat
+match A1 with
+| A1 => 1
+| A2 => 0
+end
+     : nat
+if A1 is A1 then 1 else 0
+     : nat
+if A1 is A1 then 0 else 1
+     : nat
+if Or is Sr _ then 1 else 0
+     : nat
+if Or is Sr _ then 0 else 1
+     : nat
+test =
+fun x : {True} + {True} => match x with
+                           | left t | right t => t
+                           end
+     : {True} + {True} -> True
diff --git a/test-suite/output/If.v b/test-suite/output/If.v
new file mode 100644
index 000000000000..d6fa7d07b424
--- /dev/null
+++ b/test-suite/output/If.v
@@ -0,0 +1,35 @@
+Check if true then 1 else 0.  (* boolean if *)
+
+Check if 4 then 1 else 0.  (* non boolean if, printed as if _ is *)
+
+Check if 4 is S n then n else 0.
+Check if 4 is S n then 1 else 0.
+Check if 4 is O then 1 else 0.
+
+Variant T := A | B | C.
+Check match A with A => 0 | _ => 1 end.  (* printed as match, not if *)
+Check if B is C then 1 else 0.  (* printed as if *)
+Set Printing All.
+Check if B is C then 1 else 0.  (* printed as match *)
+Unset Printing All.
+Check if B is C then 1 else 0.  (* printed as if *)
+Set Printing Regular Matches.
+Check if B is C then 1 else 0.  (* printed as match *)
+Unset Printing Regular Matches.
+Check if B is C then 1 else 0.  (* printed as if *)
+
+Variant T2 := A1 | A2.
+Check match A1 with A2 => 0 | _ => 1 end.  (* printed as match, not if *)
+Check if A1 is A1 then 1 else 0.  (* printed as if *)
+Check if A1 is A2 then 1 else 0.  (* printed as if *)
+
+Inductive natr := Sr of natr | Or.
+
+Check if Or is Sr _ then 1 else 0.
+Check if Or is Or then 1 else 0.
+
+Lemma test : sumbool True True -> True.
+Proof.
+  refine (fun x : sumbool True True => if x is left _ then _ else _);assumption.
+Defined.
+Print test.  (* printed as match (cannot use if) *)
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index fac27879494a..ce437cbf6dbb 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -17,13 +17,13 @@ option : Type -> Type
 option is template universe polymorphic
 Arguments option A%_type_scope
 Expands to: Inductive Corelib.Init.Datatypes.option
-Declared in library Corelib.Init.Datatypes, line 211, characters 10-16
+Declared in library Corelib.Init.Datatypes, line 209, characters 10-16
 option : Type@{option.u0} -> Type@{max(Set,option.u0)}
 
 option is template universe polymorphic on option.u0 (cannot be instantiated to Prop)
 Arguments option A%_type_scope
 Expands to: Inductive Corelib.Init.Datatypes.option
-Declared in library Corelib.Init.Datatypes, line 211, characters 10-16
+Declared in library Corelib.Init.Datatypes, line 209, characters 10-16
 File "./output/Inductive.v", line 27, characters 4-13:
 The command has indeed failed with message:
 Parameters should be syntactically the same for each inductive type.
diff --git a/test-suite/output/PrintGrammar.out b/test-suite/output/PrintGrammar.out
index 41bf76008457..e5bd18e3e7ee 100644
--- a/test-suite/output/PrintGrammar.out
+++ b/test-suite/output/PrintGrammar.out
@@ -80,6 +80,7 @@ Entry term is
     term 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"; 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 206ceaf73b30..05690b0eead9 100644
--- a/test-suite/output/PrintGrammarConstr.out
+++ b/test-suite/output/PrintGrammarConstr.out
@@ -33,6 +33,7 @@ Entry term is
     term 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"; as_return_type; "then"; term LEVEL "200"; "else";
     term LEVEL "200"
   | "fix"; fix_decls
diff --git a/test-suite/output/PrintGrammarTree.out b/test-suite/output/PrintGrammarTree.out
index 9721f5a454d8..78c50b19f96d 100644
--- a/test-suite/output/PrintGrammarTree.out
+++ b/test-suite/output/PrintGrammarTree.out
@@ -35,8 +35,9 @@ Entry term is
       term LEVEL "200"
     | [ "("; LIST0 name SEP ","; ")" | "()" ]; as_return_type; ":=";
       term LEVEL "200"; "in"; term LEVEL "200" ]
-  | "if"; term LEVEL "200"; as_return_type; "then"; term LEVEL "200"; "else";
-    term LEVEL "200"
+  | "if"; term LEVEL "200";
+    [ "is"; if_dthen; if_else
+    | as_return_type; "then"; term LEVEL "200"; "else"; term LEVEL "200" ]
   | "fix"; fix_decls
   | "cofix"; cofix_decls ]
 | "9" LEFTA
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index b1dec7b7d791..cac236c03518 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -63,7 +63,7 @@ comparison : Set
 
 comparison is not universe polymorphic
 Expands to: Inductive Corelib.Init.Datatypes.comparison
-Declared in library Corelib.Init.Datatypes, line 369, characters 10-20
+Declared in library Corelib.Init.Datatypes, line 367, characters 10-20
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison.
 bar : foo
@@ -105,7 +105,7 @@ nat_rect is not universe polymorphic
 Arguments nat_rect P%_function_scope O S%_function_scope n%_nat_scope
 nat_rect is transparent
 Expands to: Constant Corelib.Init.Datatypes.nat_rect
-Declared in library Corelib.Init.Datatypes, line 187, characters 0-54
+Declared in library Corelib.Init.Datatypes, line 185, characters 0-54
 
 nat_ind :
 forall P : nat -> Prop,
@@ -115,7 +115,7 @@ nat_ind is not universe polymorphic
 Arguments nat_ind P%_function_scope O S%_function_scope n%_nat_scope
 nat_ind is transparent
 Expands to: Constant Corelib.Init.Datatypes.nat_ind
-Declared in library Corelib.Init.Datatypes, line 187, characters 0-54
+Declared in library Corelib.Init.Datatypes, line 185, characters 0-54
 
 nat_sind :
 forall P : nat -> SProp,
@@ -125,7 +125,7 @@ nat_sind is not universe polymorphic
 Arguments nat_sind P%_function_scope O S%_function_scope n%_nat_scope
 nat_sind is transparent
 Expands to: Constant Corelib.Init.Datatypes.nat_sind
-Declared in library Corelib.Init.Datatypes, line 187, characters 0-54
+Declared in library Corelib.Init.Datatypes, line 185, characters 0-54
 nat_rect =
 fun (P : nat -> Type) (O : P 0) (S : forall n : nat, P n -> P (S n)) =>
 fix F (n : nat) : P n :=
diff --git a/test-suite/output/PrintKeywords.out b/test-suite/output/PrintKeywords.out
index 7dc6175218a7..5d0768262107 100644
--- a/test-suite/output/PrintKeywords.out
+++ b/test-suite/output/PrintKeywords.out
@@ -81,6 +81,7 @@ forall
 fun
 if
 in
+is
 let
 match
 of
diff --git a/test-suite/output/PrintNotation.out b/test-suite/output/PrintNotation.out
index 353f4c191900..1ff8872d0167 100644
--- a/test-suite/output/PrintNotation.out
+++ b/test-suite/output/PrintNotation.out
@@ -166,8 +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 10 with arguments constr, pattern
-at level 100 at level 100, constr, constr at level 200, no associativity.
+Notation "if _ is _ then _ else _" at level 10 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
@@ -262,8 +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 10 with arguments constr, pattern
-at level 100 at level 100, constr, constr at level 200, no associativity.
+Notation "if _ is _ then _ else _" at level 10 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/output/bug_20754.out b/test-suite/output/bug_20754.out
index ca8bcd5e7fcb..19b32da3adda 100644
--- a/test-suite/output/bug_20754.out
+++ b/test-suite/output/bug_20754.out
@@ -5,4 +5,4 @@ prod : Type -> Type -> Type
 prod is template universe polymorphic
 Arguments prod (A B)%_type_scope
 Expands to: Inductive Corelib.Init.Datatypes.prod
-Declared in library Corelib.Init.Datatypes, line 257, characters 10-14
+Declared in library Corelib.Init.Datatypes, line 255, characters 10-14
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/options.v b/test-suite/success/options.v
index f43a469405ba..f4a6207f5cfc 100644
--- a/test-suite/success/options.v
+++ b/test-suite/success/options.v
@@ -23,9 +23,7 @@ Remove Printing Coercion i.
 Test Printing Coercion for i.
 
 Test Printing Let.
-Test Printing If.
 Remove Printing Let sig.
-Remove Printing If bool.
 
 Unset Printing Synth.
 Set Printing Synth.
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/Datatypes.v b/theories/Corelib/Init/Datatypes.v
index b4c97e94e3a6..f12da4f78071 100644
--- a/theories/Corelib/Init/Datatypes.v
+++ b/theories/Corelib/Init/Datatypes.v
@@ -40,8 +40,6 @@ Inductive bool : Set :=
   | true : bool
   | false : bool.
 
-Add Printing If bool.
-
 Declare Scope bool_scope.
 Delimit Scope bool_scope with bool.
 Bind Scope bool_scope with bool.
diff --git a/theories/Corelib/Init/Notations.v b/theories/Corelib/Init/Notations.v
index 39e5157a4ae8..8823f6212f6b 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 10, v at level 200, p pattern at level 100).
+  (at level 10, c, u, v at level 200, p pattern at level 100).
 
 End IfNotations.
 
diff --git a/theories/Corelib/Init/Specif.v b/theories/Corelib/Init/Specif.v
index cce9c205a6ce..b78e563f1f48 100644
--- a/theories/Corelib/Init/Specif.v
+++ b/theories/Corelib/Init/Specif.v
@@ -910,8 +910,6 @@ Inductive sumbool (A B:Prop) : Set :=
   | right : B -> {A} + {B}
  where "{ A } + { B }" := (sumbool A B) : type_scope.
 
-Add Printing If sumbool.
-
 Arguments left {A B} _, [A] B _.
 Arguments right {A B} _ , A [B] _.
 
@@ -926,8 +924,6 @@ Inductive sumor (A:Type) (B:Prop) : Type :=
   | inright : B -> A + {B}
  where "A + { B }" := (sumor A B) : type_scope.
 
-Add Printing If sumor.
-
 Arguments inleft {A B} _ , [A] B _.
 Arguments inright {A B} _ , A [B] _.