{"shas":[["7a7a09378e492b5b2dc87e3a8e502e842ca1faf5","a45fbbdd74cedccba89b73bcb3a4a86a54c9047c@85f007b7-540e-0410-9357-904b9bb8a0f7","Add 'Existing Instances' declaration to declare multiple instances at once.\n\nThis is useful, for example, in declaring the projection of the dependent\nrecord bundled form of an unbundled typeclass.\n\nPatch submitted by Tom Prince\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7","letouzey"],["bdac8f996a89701f74a5fcb649ec12bc3aaa9d07","bae1360c009e66c9e01104e812ccd4e2858da25a@85f007b7-540e-0410-9357-904b9bb8a0f7","Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.\n\nPatch submitted by Tom Prince.\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13957 85f007b7-540e-0410-9357-904b9bb8a0f7","aspiwack"],["bb774b704c45ee182669e133115ea606d595a004","a45fbbdd74cedccba89b73bcb3a4a86a54c9047c@85f007b7-540e-0410-9357-904b9bb8a0f7","Fix dev/base_include after change of constant_body\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13958 85f007b7-540e-0410-9357-904b9bb8a0f7","letouzey"],["9600a6960debedbe1bc941aff383fab37a546b94","2103b717912084dbff9bf6b8b5db96c766e38868@85f007b7-540e-0410-9357-904b9bb8a0f7","A few extra combinators about rel_declaration/named_declaration + a bit of doc\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7","herbelin"],["b2b2292949b04ec7d114addd487f6e0a94003914","2103b717912084dbff9bf6b8b5db96c766e38868@85f007b7-540e-0410-9357-904b9bb8a0f7","Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)\n(backport from 8.3)\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7","herbelin"],["5de2bbd213eb770ba465c67103004d9286444a63","a45fbbdd74cedccba89b73bcb3a4a86a54c9047c@85f007b7-540e-0410-9357-904b9bb8a0f7","Extraction: avoid some useless Obj.magic by fixing my ML type unifier\n\n Due to wrong pattern order in Mlutil.mgu, simple situations like\n ?n == ?n were considered unsolvable as soon as one side was aliased\n (i.e. inside an instantiated type meta).\n\n Moreover, use general equality as last resort, instead of forgetting\n cases like Taxiom == Taxiom.\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13963 85f007b7-540e-0410-9357-904b9bb8a0f7","letouzey"],["92a5f74259977cc3f92d8b822bdb727a95e64bc6","a45fbbdd74cedccba89b73bcb3a4a86a54c9047c@85f007b7-540e-0410-9357-904b9bb8a0f7","Extraction: unfolds the let-in created by Program when handling \"match\"\n\n This leads to code closer to the original input of the user,\n and moreover some more dummy __ may be removed this way.\n\n To avoid unfolding by mistake user's variables, we change\n the name of these generated let-in into \"program_branch_NN\" instead\n of \"branch_NN\"\n\ngit-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7","letouzey"]],"repo":"tomprince/coq","actor":"tomprince","ref":"refs/heads/trunk","size":7,"head":"92a5f74259977cc3f92d8b822bdb727a95e64bc6","actor_gravatar":"e81edff3af564b86f4c9d780a8023299","push_id":28511779}