X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=15645951e29a0af9920195a60dca96ff8ce9d2ec;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=b75e2da8911b1cff99c081ae383960a08999db9a;hpb=2e9230cc95280f928b15c624ee4564fffea56373;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index b75e2da89..15645951e 100644
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -94,9 +94,9 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
    let _,metasenv,_,_ = proof in
     let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let old_context_len = List.length context in
-     let termty = CicTypeChecker.type_of_aux' metasenv context term in
-
-      let rec make_list termty = 
+     let termty,_ = 
+       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+     let rec make_list termty = 
       (* N.B.: altamente inefficente? *)
        let rec search_inductive_types urilist termty =
         (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
@@ -136,7 +136,9 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
           let _,metasenv,_,_ = proof in
            let _,context,_ = CicUtil.lookup_meta goal metasenv in
             let old_context_len = List.length context in
-            let termty = CicTypeChecker.type_of_aux' metasenv context term' in
+            let termty,_ = 
+	      CicTypeChecker.type_of_aux' metasenv context term' 
+		CicUniv.empty_ugraph in
              warn ("elim_clear termty= " ^ CicPp.ppterm termty);
              match termty with
                 C.MutInd (uri,typeno,exp_named_subst)