aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-20 18:46:08 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-20 18:46:08 +0000
commitdebb1dba19c079afd7657e8518034209f08bb2b1 (patch)
tree65ed66a015b5bab33ac7d51dde167ca37f757928 /toplevel/toplevel.mli
parent17ca9766c45ebb368558712eff18d0ed71583e66 (diff)
Fix interface of resolve_typeclasses: onlyargs -> with_goals:
by default typeclass resolution is not launched on goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/toplevel.mli')
0 files changed, 0 insertions, 0 deletions