X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=0a1f13a78ffd0d04072c223fbdcdda06c39f4068;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=62c2adab57e2e9f34e04c7ca1fff6c50fa9d828b;hpb=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 62c2adab5..0a1f13a78 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -206,7 +206,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
@@ -298,14 +298,14 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     S.lift (k-1) (find_image t)
    with Not_found ->
     match t with
-       C.Rel n as t ->
+       C.Rel n ->
         if n < k then C.Rel n else C.Rel (n + nnn)
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
         in
          C.Var (uri,exp_named_subst')
-     | C.Meta (i, l) as t -> 
+     | C.Meta (i, l) -> 
         let l' =
          List.map
           (function
@@ -450,7 +450,7 @@ let reduce context =
        in
         let t' = C.MutInd (uri,i,exp_named_subst') in
          if l = [] then t' else C.Appl (t'::l)
-    | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
@@ -459,10 +459,7 @@ let reduce context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
-            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -473,9 +470,6 @@ let reduce context =
               in
                reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
-            in
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -600,14 +594,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let mk_appl t l =
-   if l = [] then 
-     t 
-   else 
-     match t with
-     | Cic.Appl l' -> Cic.Appl (l'@l)
-     | _ -> Cic.Appl (t::l)
- in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
@@ -697,9 +683,7 @@ let simpl context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -721,7 +705,7 @@ let simpl context =
                  body
               in
                let tl' = List.map (reduceaux context []) tl in
-                reduceaux context tl body'
+                reduceaux context tl' body'
          | t -> t
        in
         (match decofix (CicReduction.whd context term) with
@@ -818,7 +802,7 @@ let simpl context =
     let res,constant_args =
      let rec aux rev_constant_args l =
       function
-         C.Lambda (name,s,t) as t' ->
+         C.Lambda (name,s,t) ->
           begin
            match l with
               [] -> raise WrongShape
@@ -829,11 +813,7 @@ let simpl context =
           end
        | C.LetIn (_,s,t) ->
           aux rev_constant_args l (S.subst s t)
-       | C.Fix (i,fl) as t ->
-          let tys =
-           List.map (function (name,_,ty,_) ->
-            Some (C.Name name, C.Decl ty)) fl
-          in
+       | C.Fix (i,fl) ->
            let (_,recindex,_,body) = List.nth fl i in
             let recparam =
              try