aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
authorgareuselesinge2013-10-03 09:09:22 +0000
committergareuselesinge2013-10-03 09:09:22 +0000
commitc1388ce6338742ab20aea9774e6510f43d7697ff (patch)
tree32eeb4b1420cec7745a3f1008fd832f7b44723a1 /pretyping/typeclasses_errors.ml
parentc92af9e12b95b731e04834c3d28cde3a80156e9b (diff)
STM: delegate proofs to slaves only if they are not trivial
Still too simple and not configurable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions