(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From Coq Require Export ssreflect. Global Set SsrOldRewriteGoalsOrder. Global Set Asymmetric Patterns. Global Set Bullet Behavior "None".