From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 24 May 2005 13:33:35 +0000 (+0000)
Subject: fixed syntax
X-Git-Tag: single_binding~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=90f02ec7eb997c4d4961dabcfce04d26bb77ca91;p=helm.git

fixed syntax
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 5e70ff571..8e02154ab 100644
--- 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 570ab894e..0f169fc27 100644
--- 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));