- Cleanup parsing of binders, reducing to a single production for all

  binders.
- Change syntax of type class instances to better match the usual syntax of
  lemmas/definitions with name first, then arguments ":" instance.
  Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
  documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
  Program.Utils, and subset_scope as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 2 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 481b73fd0..01b309f3c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -442,10 +442,8 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
-    let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
     let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
-    let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
     let appl_arg = Gram.Entry.create "constr:appl_arg"
   end