X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=66a9c0930e934e21070e4a0bb0d85e762d5899d9;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=0cb8aceadbaaf3a14bbc43d95fd65897b7a53468;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 0cb8acead..66a9c0930 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -204,12 +204,8 @@ let
 =
  let module C = Cic in
   let params =
-    let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
-      match o with
-	  C.Constant (_,_,_,params)
-	| C.CurrentProof (_,_,_,_,params)
-	| C.Variable (_,_,_,params)
-	| C.InductiveDefinition (_,params,_) -> params
+    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    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
@@ -220,9 +216,9 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-	    let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+	    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)
@@ -492,9 +488,9 @@ let elim_tac ~term =
      let eliminator_uri =
       let buri = U.buri_of_uri uri in
       let name = 
-	let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+	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