aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorherbelin2003-04-07 17:19:41 +0000
committerherbelin2003-04-07 17:19:41 +0000
commit928287134ab9dd23258c395589f8633e422e939f (patch)
tree192971793635b1057b78004b14df4ad5dfac9561 /dev/base_include
parentc4ef643444acecdb4c08a74f37b9006ae060c5af (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@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions