From 4b98ed995936425fc85b3e5e81bf14caf2e01a30 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 16:36:21 +0000
Subject: [PATCH] New change in patterns: the pattern "in H" is now interpreted
 as "in H \vdash ?". It used to be interpreted as "in H \vdash %".

---
 helm/ocaml/cic_notation/grafiteParser.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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
    ]
-- 
2.39.2