Commit e6be251d authored by Janno's avatar Janno

Make `iStartProof` monomorphic to save 1-2sec.

parent 45e1d49b
......@@ -73,7 +73,7 @@ Inductive iGoal : Type :=
Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ P.
Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
Monomorphic Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with
| [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist goal) with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment