X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=d2fa70184dc87169ebc5feae4180271faf2fcf3a;hb=fd991956035d0f1b663aab48325097e53ed9e00e;hp=8c58b33c2e4410191b1885edfc2c5448dc5a1000;hpb=f42d23df32484582ebba6fdafd23e873c0acf90d;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 8c58b33c2..d2fa70184 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -166,12 +166,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