]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite_parser/grafiteParser.ml
Big commit to let Ferruccio try the merge_coercion patch.
[helm.git] / helm / ocaml / grafite_parser / grafiteParser.ml
index 64db522950c31e50e788c07878ced0dc5775d2d9..f76528567f3387a794bf57027c5c5ff87b5c23c4 100644 (file)
@@ -304,7 +304,9 @@ EXTEND
     name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
-       name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) 
+       name = IDENT ; 
+       coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; 
+       ty = term -> (name,ty,coercion) 
      ] SEP SYMBOL ";"; SYMBOL "}" -> 
       let params =
         List.fold_right