New change in patterns: the pattern "in H" is now interpreted as

"in H \vdash ?". It used to be interpreted as "in H \vdash %".

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index ae7e5229d1941d2809023f51863295cace796659..4a21e10b5a9e6334ce022bbb430b6ba6739fb08f 100644 (file)
--- 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
    ]