From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 12:25:36 +0000 (+0000)
Subject: - bugfix: raise an Invalid_choice insteda of a generic exception on
X-Git-Tag: V_0_5_1_4~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9e00ee3e8d57c51e52fcfca9c642b8f366b8d0d;p=helm.git

- bugfix: raise an Invalid_choice insteda of a generic exception on
  inductive constructor error
- moved TEST_INTERPRETATION debug message in a better place
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index aa3fe97ee..b2df644d2 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -23,7 +23,10 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 open Disambiguate_types
+open UriManager
 
 exception Invalid_choice
 exception No_choices of domain_item
@@ -59,6 +62,7 @@ type test_result =
 
 let refine metasenv context term =
   let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
+  debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
   try
     let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
     Ok (term', metasenv')
@@ -78,10 +82,6 @@ let refine metasenv context term =
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
-open Printf
-
-open UriManager
-
 let indtyuri_of_uri uri =
   let index_sharp =  String.index uri '#' in
   let index_num = index_sharp + 3 in
@@ -166,7 +166,7 @@ let interpretate ~context ~env ast =
           match resolve env (Id indty_ident) () with
           | Cic.MutInd (uri, tyno, _) -> uri, tyno
           | Cic.Implicit -> raise Try_again
-          | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident)
+          | _ -> raise Invalid_choice
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
@@ -389,8 +389,6 @@ module Make (C: Callbacks) =
           let cic_term =
             interpretate ~context:disambiguate_context ~env:filled_env term
           in
-          debug_print
-            (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm cic_term));
           refine metasenv context cic_term
         with
         | Try_again -> Uncertain