Initial revision

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index b85be0754e7194cd9efc140d365d4295339915c6..af67f1c1454a8a367ef033b3034e1275b4be7aa0 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -123,7 +123,9 @@ expr2:
         Hashtbl.find uri_of_id_map $1
        with
         Not_found ->
-         raise (UnknownIdentifier $1)
+        match ! CicTextualParser0.locate_object $1 with
+         | None      -> raise (UnknownIdentifier $1)
+         | Some term -> Hashtbl.add uri_of_id_map $1 term; term  
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let cookingno = get_cookingno (fst $5) in