aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:08 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:08 +0000
commit6d5eee245a85f410ec184353ab9f38ce3aa4e331 (patch)
tree9260a0fb3662dbeb6837468e30f69f5f862e7893 /ide/ideutils.mli
parent3b7ecfa6d4da684a635b2469c2d9a2e1e0ed0807 (diff)
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
**Warning** the ml code of plugins may have to be adapted after this. Concerning coq itself, I've done the adaptations, let's hope I've forgotten none. In practice, the number of changes are relatively low, and the code is quite cleaner this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
0 files changed, 0 insertions, 0 deletions