checked in new version of matita from svn

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

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