coq - 使用功能方案解决 CoqIDE 8.11 的“vernac 的非法开始”错误

Question

我在某种程度上是 Coq 的新手，使用 CoqIDE 8.11，并且看不出我在这里做错了什么。我检查了文档，但没有找到解决问题的方法。

和

Functional Scheme insert_ind := Induction for insert Sort Prop.
Check insert_ind.

我收到一条Syntax error: illegal begin of vernac.消息。知道插入之前定义如下：

Fixpoint insert l a :=
match l with
| nil => (a::nil)
| (b::l) =>
  match preOrdreImplem a b with
  | true => a::b::l
  | false => b:: (insert l a)
  end
end.

而且我已经在引理部分使用它并且没有遇到任何问题。非常感谢任何帮助或提示。