Use correct scheme kind for CarriersTermAlgebra_ind

Elimination is documented as nonrecursive although incorrectly behaves like Induction until coq/coq#19017
HoTT · May 14, 2024 · 5a54a54 · 5a54a54
1 parent 23d4007
commit 5a54a54
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 σ.