- coercion now requires an URI

[helm.git] / helm / ocaml / grafite_parser / grafiteParser.ml

diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index f76528567f3387a794bf57027c5c5ff87b5c23c4..aa60c87c43267e823461716190a859050117c26b 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteParser.ml
+++ b/helm/ocaml/grafite_parser/grafiteParser.ml
@@ -72,9 +72,9 @@ EXTEND
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
       let goal_path =
        match goal_path, hyp_paths with
-          None, [] -> Ast.UserInput
-        | None, _::_ -> Ast.Implicit
-        | Some goal_path, _ -> goal_path
+          None, [] -> Some Ast.UserInput
+        | None, _::_ -> None
+        | Some goal_path, _ -> Some goal_path
       in
        hyp_paths,goal_path
    ]
@@ -91,12 +91,12 @@ EXTEND
         ] ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
-             wanted,None -> wanted, [], Ast.UserInput
+             wanted,None -> wanted, [], Some Ast.UserInput
            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
          in
           wanted, hyp_paths, goal_path ] ->
       match res with
-         None -> None,[],Ast.UserInput
+         None -> None,[],Some Ast.UserInput
        | Some ps -> ps]
   ];
   direction: [
@@ -476,10 +476,8 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true)
-    | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true)
+    | IDENT "coercion" ; suri = URI ->
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
     | IDENT "alias" ; spec = alias_spec ->
         GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->