aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2003-04-07 17:36:44 +0000
committerherbelin2003-04-07 17:36:44 +0000
commit4ab520180b7597f8358f9d351151cd73e43858a3 (patch)
tree0d8bdd472bedc71ec0bc9bee6f6dd66fde03dba6 /dev
parent928287134ab9dd23258c395589f8633e422e939f (diff)
Globalisation des noms de tactiques dans les définitions de tactiques
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions