The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Jun 20, 2013 at 07:06:19PM +0200, Pierre-Marie Pédrot wrote:
> For now, it is still quite dumb as you mentioned, as a process is
> forked for each subgoal. It is really a hack, and it would need any
> polishing to be useful, but I wanted to advertise it nonetheless.

I did not look at the code, but I'm curious.  What happens if you do:

  assert True >> [ abstract( exact I ) | idtac ].

And in the even more trickier case, if you do:

  Goal (Type /\ Type) /\ True.
  split; [ split >> [ exact Type | exact Type ] | exact Type ].

which is the resulting proof term?
 (Conj (Conj Type_i Type_i) Type_i)  or  (Conj (Conj Type_i Type_j) Type_k)

Ciao
-- 
Enrico Tassi