X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=66a9c0930e934e21070e4a0bb0d85e762d5899d9;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=92b89a679c987c293e4395f993930707c5ad3d2b;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 92b89a679..66a9c0930 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -205,11 +205,7 @@ let
  let module C = Cic in
   let params =
     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      match o with
-	  C.Constant (_,_,_,params)
-	| C.CurrentProof (_,_,_,_,params)
-	| C.Variable (_,_,_,params)
-	| C.InductiveDefinition (_,params,_) -> params
+    CicUtil.params_of_obj o
   in
    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
     let next_fresh_meta = ref newmeta in
@@ -222,7 +218,7 @@ let
           let ty =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-		  C.Variable (_,_,ty,_) ->
+		  C.Variable (_,_,ty,_,_) ->
 		    CicSubstitution.subst_vars !exp_named_subst_diff ty
 		| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
           in
@@ -386,7 +382,7 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
  let cut_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
@@ -494,7 +490,7 @@ let elim_tac ~term =
       let name = 
 	let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
-          C.InductiveDefinition (tys,_,_) ->
+          C.InductiveDefinition (tys,_,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in
             name
         | _ -> assert false