aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorwerner2001-04-24 17:30:03 +0000
committerwerner2001-04-24 17:30:03 +0000
commit88bc6a84e38ede558386be3eef1d1515af85ea21 (patch)
tree901ecbacc282eb809058a84d4c80875d9d8f667a /dev
parent5c0fb1246294ca1a7144af64fa1bdc198c0d24f1 (diff)
interdiction occ positives ET negatives dans Pattern
(en fait dans term.ml, fonction subst_occ_gen BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1698 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions