- attributes support

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 92b89a679c987c293e4395f993930707c5ad3d2b..66a9c0930e934e21070e4a0bb0d85e762d5899d9 100644 (file)
--- 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