--------------------- The tactic language --------------------- :Source: https://coq.inria.fr/distrib/current/refman/ltac.html :Converted by: Maxime Dénès