- 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 aa3fe97eed492af74115692780f0e66f79d87a50..b2df644d261b087c60068ba971294a0d3894a7c2 100644 (file)
--- 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