X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=590b482c716db80b74b83429aa4808fbb804aa38;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=21fc2b33c1f60aa1d1ded2a76fa812a4992ea97e;hpb=b8ac0d11d5cd4083838a3848fce68683a518b54a;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 21fc2b33c..590b482c7 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -276,8 +276,8 @@ let discriminate'_tac ~term =
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd(LibraryObjects.false_URI,0,[]))
-                                     else (C.MutInd(LibraryObjects.true_URI,0,[]))
+                                     then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+                                     else (C.MutInd(LibraryObjects.true_URI (),0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -287,7 +287,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
 		     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(LibraryObjects.false_URI,0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with