Merge pull request #1958 from SkySkimmer/scheme-norec

Use correct scheme kind for CarriersTermAlgebra_ind
HoTT · May 14, 2024 · 1a1edfa · 1a1edfa
2 parents 71f9cb8 + 3e616d0
commit 1a1edfa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Algebra/Universal/TermAlgebra.v b/theories/Algebra/Universal/TermAlgebra.v
@@ -30,7 +30,7 @@ Inductive CarriersTermAlgebra {σ} (C : Carriers σ) : Carriers σ :=
       DomOperation (CarriersTermAlgebra C) (σ u) ->
       CarriersTermAlgebra C (sort_cod (σ u)).
 
-Scheme CarriersTermAlgebra_ind := Elimination for CarriersTermAlgebra Sort Type.
+Scheme CarriersTermAlgebra_ind := Induction for CarriersTermAlgebra Sort Type.
 Arguments CarriersTermAlgebra_ind {σ}.
 
 Definition CarriersTermAlgebra_rect {σ} := @CarriersTermAlgebra_ind σ.