merged cic_notation with disambiguation: good luck!

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index e52baffdda60883f60bb8fa04f38a354b73344dc..c9a5fbafba473c5f0d604db95ca7772731bc2c21 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -40,16 +40,6 @@ let min_precedence = 0
 let max_precedence = 100
 let default_precedence = 50
 
-let let_in_prec = 10
-let binder_prec = 20
-let apply_prec = 70
-let simple_prec = 90
-
-let let_in_assoc = Gramext.NonA
-let binder_assoc = Gramext.RightA
-let apply_assoc = Gramext.LeftA
-let simple_assoc = Gramext.NonA
-
 let level1_pattern =
   Grammar.Entry.create level1_pattern_grammar "level1_pattern"
 let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
@@ -59,10 +49,6 @@ let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
 let return_term loc term = ()
 
-let fail floc msg =
-  let (x, y) = loc_of_floc floc in
-  failwith (sprintf "Error at characters %d - %d: %s" x y msg)
-
 let int_of_string s =
   try
     Pervasives.int_of_string s
@@ -578,7 +564,7 @@ EXTEND
         SYMBOL "]" ->
           return_term loc (Case (t, indty_ident, outtyp, patterns))
       | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
-          return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ])
+          return_term loc (Cast (p1, p2))
       | LPAREN; p = term; RPAREN -> p
       | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
       ]