From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 23 May 2011 23:08:04 +0000 (+0000)
Subject: 1) interpretation of matches in patterns implemented
X-Git-Tag: make_still_working~2495
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4665bcba9c87ecced8746f08da717c767b1a839;p=helm.git

1) interpretation of matches in patterns implemented
2) missing exception added to matitaExcPp
---

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
diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml
index 5ecea5dc8..5134f4039 100644
--- a/matita/matita/matitaExcPp.ml
+++ b/matita/matita/matitaExcPp.ml
@@ -169,6 +169,8 @@ let rec to_string =
      None, "NCicUnification uncertain: " ^ Lazy.force msg
   | DisambiguateChoices.Choice_not_found msg ->
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
+  | DisambiguateTypes.Invalid_choice msg ->
+     None, ("Invalid choice: " ^ snd (Lazy.force msg))
   | MatitaEngine.EnrichedWithStatus (exn,_) ->
      None, snd(to_string exn)
   | NTacStatus.Error (msg,None) ->