X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=4a21e10b5a9e6334ce022bbb430b6ba6739fb08f;hb=3e8363bec852afb37160d8144db8d94bbff447d6;hp=ae7e5229d1941d2809023f51863295cace796659;hpb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index ae7e5229d..4a21e10b5 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -69,9 +69,10 @@ EXTEND
        SEP SYMBOL ";";
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
       let goal_path =
-       match goal_path with
-          None -> Ast.UserInput
-        | Some goal_path -> goal_path
+       match goal_path, hyp_paths with
+          None, [] -> Ast.UserInput
+        | None, _::_ -> Ast.Implicit
+        | Some goal_path, _ -> goal_path
       in
        hyp_paths,goal_path
    ]