From b3f366c0fa3fcadcf5f21913f71a2bce591e47d0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 May 2011 09:33:31 +0000 Subject: [PATCH] Syntax for coercion nocomposites fixed. --- matita/components/grafite_parser/grafiteParser.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 762da10f5..ff36dbe21 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -576,10 +576,12 @@ EXTEND G.NUnivConstraint (loc,u1,u2) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> G.UnificationHint (loc, t, n) - | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term; + | IDENT "coercion"; name = IDENT; + compose = OPT [ IDENT "nocomposites" -> () ]; + SYMBOL ":"; ty = term; SYMBOL <:unicode>; t = term; "on"; id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term; - "to"; target = term; compose = OPT [ IDENT "nocomposites" -> () ] -> + "to"; target = term -> let compose = compose = None in G.NCoercion(loc,name,compose,t,ty,(id,source),target) | IDENT "record" ; (params,name,ty,fields) = record_spec -> -- 2.39.2