The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi all,

I am puzzled by the behaviour of the change tactics.
I hope that someone can enlighten me.

My problem is that I have a conversion that does not terminate.
I am in the context of an automatic tactic 
and I would like to have a robust (and fast) alternative.

Consider the following:
* change term (* Takes forever. Fine, probably this is sometimes unavoidable. 
*)

* change_no_check term;
        (* bound to Tactics.convert_concl_no_check (snd term) DEFAULTcast  
            which performs a change blindly without checking that terms are 
convertible
         *)
  tac.
Time  Qed.  (* Finished transaction in 0.012 secs (0.012u,0.s) (successful)*)

Is-it always a sound course of action to wrap an « abstract » around a tactic 
and perform conversion without check within the tactic ?


* match goal with
   |  |- ?X => replace X with term by reflexivity
  end;  (* Is instantaneous *)
  tac.   
Time Qed.  (*Finished transaction in 0.015 secs (0.015u,0.s) (successful) *)

Is-it a safer path to insert an explicit equality at the cost of a slightly 
bigger term ?

What do you think ?

Thanks,

—
Frédéric