aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/gmap.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-11 21:49:26 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-11 21:49:26 +0000
commit3e5b93760241671c8959da1cdb8023cfa7f62987 (patch)
treec8f1d8b492b4efca26d9e442165b92532f34656c /lib/gmap.ml
parent0601db38b579513e4ab39a161591cd359260490e (diff)
Better compatibility for Peqb
As show by contrib TreeAutomata, the Peqb now placed in BinPos was using 1st arg as "struct", instead of 2nd arg as earlier. Fix that, and remove the "Import BinPos BinNat" hack in Ndec (merci Hugo :-). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12503 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/gmap.ml')
0 files changed, 0 insertions, 0 deletions