aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/leminv.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-23 23:01:37 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-23 23:01:37 +0000
commit85c65e07e70e7001b3048ea01c40b052da42293c (patch)
tree208544fabab99ff634f2395c87a6c1b66470a48b /tactics/leminv.ml
parente50635edb2504712ae9b88951e155549adfc5d04 (diff)
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/leminv.ml')
0 files changed, 0 insertions, 0 deletions