X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=8e3f267775535c4bba5ae5216ba3af11cd1d77bf;hb=225887a9f23aac79d4cca907da026917b7df04dc;hp=5c2de5caa90ba4e22758637b4feb54478d22ae35;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 5c2de5caa..8e3f26777 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -18,8 +18,8 @@ open DisambiguateTypes
 module Ast = NotationPt
 module NRef = NReference 
 
-let debug_print s = prerr_endline (Lazy.force s);;
-let debug_print _ = ();;
+let debug = ref false;;
+let debug_print s = if !debug then prerr_endline (Lazy.force s);;
 
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
@@ -66,6 +66,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c
 let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
  ~localization_tbl 
 =
+  (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
   assert (metasenv=[]);
   assert (subst=[]);
   let localise t = 
@@ -117,12 +118,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
          NCicUntrusted.NCicHash.add localization_tbl res loc;
        res
     | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
-    | NotationPt.Appl (NotationPt.Appl inner :: args) ->
-        aux ~localize loc context (NotationPt.Appl (inner @ args))
     | NotationPt.Appl 
-        (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
+        (NotationPt.AttributedTerm (att, inner)::args)->
         aux ~localize loc context 
-          (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+          (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args)))
+    | NotationPt.Appl (NotationPt.Appl inner :: args) ->
+        aux ~localize loc context (NotationPt.Appl (inner @ args))
     | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux ~localize loc context) args in
         Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
@@ -166,12 +167,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                 raise (DisambiguateTypes.Invalid_choice 
                  (lazy (loc, "Syntax error: the left hand side of a "^
                    "branch pattern must be \"_\"")))
-           ) branches
+           ) branches in
+         let indtype_ref =
+          NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
          in
-         (*
-          NCic.MutCase (ref, cic_outtype, cic_term,
-            (List.map do_branch branches))
-          *) ignore branches; assert false (* patterns not implemented yet *)
+          NCic.Match (indtype_ref, cic_outtype, cic_term,
+           (List.map do_branch branches))
         else
          let indtype_ref =
           match indty_ident with