fixed syntax

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 5e70ff571ecd62b8a3402da395c8aebee9b5312a..8e02154ab994c1fcffb0626fdd6e9a93a06f135f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -391,7 +391,7 @@ EXTEND
         (match (pat, terms) with
         | None, [] -> TacticAst.Reduce (loc, kind, None)
         | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
-        | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+        | Some pat, [] -> fail loc "Missing term [list]"
         | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
     | [ IDENT "reflexivity" ] ->
         TacticAst.Reflexivity loc

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 570ab894e434e7b9f45b5444e854c14b09fda6fe..0f169fc27ee65da0cd07920b10870fbf99ade62c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -471,6 +471,7 @@ module Make (C: Callbacks) =
           (function None -> Cic.Anonymous | Some (name, _) -> name)
           context
       in
+      debug_print ("TERM IS: " ^ (CicAstPp.pp_term term));
       let term_dom = domain_of_term ~context:disambiguate_context term in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain term_dom));