X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=c413d4694e266ae35a48f76f18bf1878217689f2;hb=60c7321771851b82493bb202185ee184f1e7a3d1;hp=4a349e54c4a6976ede342383052f034dcbf124d1;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 4a349e54c..c413d4694 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -275,8 +275,8 @@ prerr_endline ("XXXX nth funzionano ") ;
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
-                                     else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
+                                     then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
+                                     else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -285,7 +285,7 @@ prerr_endline ("XXXX nth funzionano ") ;
 
                     let (proof',goals') = 
                      EliminationTactics.elim_type_tac 
-                      ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) 
+                      ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
                       ~status 
                     in
                      (match goals' with