The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Without understanding what the pretyper does, is the implication of not 
having any backtracking in the pretyper that Coq can't change the 
decision about the type of any term once it is typed?  That would indeed 
explain why backtracking back into typeclass instance search couldn't be 
made to work.

Does this restriction on backtracking in the pretyper also imply that 
experimental typed alternatives to LTac, such as MTac, would all be 
incapable of backtracking after a successful solution of a type?  If so, 
would the potential solution of the issue for tactic-in-term also 
improve the situation for MTac-like alternatives?

-- Jonathan

On 03/13/2016 05:29 AM, Arnaud Spiwack wrote:
> Possibly. In that case we'd have a much cleaner story for tactics in terms. 
> But
> this would probably be the only source of backtracking in the pretyper, if I'm
> not mistaken.
>
> On 12 March 2016 at 13:51, Pierre-Marie Pédrot 
> <pierre-marie.pedrot AT inria.fr
> <mailto:pierre-marie.pedrot AT inria.fr>>
>  wrote:
>
>      On 11/03/2016 21:58, Arnaud Spiwack wrote:
>      > Of course, for Coq, this is probably unworkable. Pretyping is the most
>      > sensitive part of Coq and making everything subtly different in
>      > unpredictable ways is probably not worth the huge effort this would
>      > represent.
>
>      I'm not sure that the pretyper by itself would be difficult to port to
>      the monad, at least for the pretyping.ml <http://pretyping.ml> file. This
>      would make it
>      compatible with the tactic-in-term bactracking. What would be more
>      difficult would be the unification stuff.
>
>      PMP