X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=21f2cbebf72aa68f375e204345dbed3a52b717c0;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=bb724fc758d2736c40a7c199b60898501fe4308a;hpb=86122a3ce11bdf45ecb93f8f7efaffa49bd31fa2;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index bb724fc75..21f2cbebf 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -37,47 +37,47 @@
 (* The code of this module is derived from the code of CicReduction *)
 
 exception Impossible of int;;
-exception ReferenceToDefinition;;
-exception ReferenceToAxiom;;
+exception ReferenceToConstant;;
 exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
 exception RelToHiddenHypothesis;;
 
-(* syntactic_equality up to cookingsno for uris *)
-(* (which is often syntactically irrilevant)    *)
-let syntactic_equality ~alpha_equivalence =
+let alpha_equivalence =
  let module C = Cic in
   let rec aux t t' =
    if t = t' then true
    else
     match t,t' with
-       C.Rel _, C.Rel _
-     | C.Var _, C.Var _
-     | C.Meta _, C.Meta _
-     | C.Sort _, C.Sort _
-     | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+       C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
+        UriManager.eq uri1 uri2 &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
      | C.Cast (te,ty), C.Cast (te',ty') ->
         aux te te' && aux ty ty'
-     | C.Prod (n,s,t), C.Prod (n',s',t') ->
-        (alpha_equivalence || n = n') && aux s s' && aux t t'
-     | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
-        (alpha_equivalence || n = n') && aux s s' && aux t t'
-     | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
-        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.Prod (_,s,t), C.Prod (_,s',t') ->
+        aux s s' && aux t t'
+     | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+        aux s s' && aux t t'
+     | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+        aux s s' && aux t t'
      | C.Appl l, C.Appl l' ->
         (try
           List.fold_left2
            (fun b t1 t2 -> b && aux t1 t2) true l l'
          with
           Invalid_argument _ -> false)
-     | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
-     | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
-        UriManager.eq uri uri' && i = i'
-     | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
-        UriManager.eq uri uri' && i = i' && j = j'
-     | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+     | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
+        UriManager.eq uri uri' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
+        UriManager.eq uri uri' && i = i' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutConstruct (uri,i,j,exp_named_subst1),
+       C.MutConstruct (uri',i',j',exp_named_subst2) ->
+        UriManager.eq uri uri' && i = i' && j = j' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
         UriManager.eq sp sp' && i = i' &&
          aux outt outt' && aux t t' &&
           (try
@@ -89,23 +89,31 @@ let syntactic_equality ~alpha_equivalence =
         i = i' &&
         (try
           List.fold_left2
-           (fun b (name,i,ty,bo) (name',i',ty',bo') ->
-             b && (alpha_equivalence || name = name') && i = i' &&
-              aux ty ty' && aux bo bo') true fl fl'
+           (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+             b && i = i' && aux ty ty' && aux bo bo'
+           ) true fl fl'
          with
           Invalid_argument _ -> false)
      | C.CoFix (i,fl), C.CoFix (i',fl') ->
         i = i' &&
         (try
           List.fold_left2
-           (fun b (name,ty,bo) (name',ty',bo') ->
-             b && (alpha_equivalence || name = name') &&
-              aux ty ty' && aux bo bo') true fl fl'
+           (fun b (_,ty,bo) (_,ty',bo') ->
+             b && aux ty ty' && aux bo bo'
+           ) true fl fl'
          with
           Invalid_argument _ -> false)
-     | _,_ -> false
- in
-  aux
+     | _,_ -> false (* we already know that t != t' *)
+  and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
+   try
+     List.fold_left2
+      (fun b (uri1,t1) (uri2,t2) ->
+        b && UriManager.eq uri1 uri2 && aux t1 t2
+      ) true exp_named_subst1 exp_named_subst2
+    with
+     Invalid_argument _ -> false
+  in
+   aux
 ;;
 
 (* "textual" replacement of a subterm with another one *)
@@ -115,7 +123,8 @@ let replace ~equality ~what ~with_what ~where =
    function
       t when (equality t what) -> with_what
     | C.Rel _ as t -> t
-    | C.Var _ as t  -> t
+    | C.Var (uri,exp_named_subst) ->
+       C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
     | C.Meta _ as t -> t
     | C.Sort _ as t -> t
     | C.Implicit as t -> t
@@ -128,12 +137,16 @@ let replace ~equality ~what ~with_what ~where =
        (match List.map aux l with
            (C.Appl l')::tl -> C.Appl (l'@tl)
          | l' -> C.Appl l')
-    | C.Const _ as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-       C.MutCase (sp,cookingsno,i,aux outt, aux t,
-        List.map aux pl)
+    | C.Const (uri,exp_named_subst) ->
+       C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+    | C.MutInd (uri,i,exp_named_subst) ->
+       C.MutInd
+        (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
+       C.MutConstruct
+        (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+    | C.MutCase (sp,i,outt,t,pl) ->
+       C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
     | C.Fix (i,fl) ->
        let substitutedfl =
         List.map
@@ -161,7 +174,11 @@ let replace_lifting ~equality ~what ~with_what ~where =
    function
       t when (equality t what) -> S.lift (k-1) with_what
     | C.Rel n as t -> t
-    | C.Var _ as t  -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        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 -> 
        let l' =
         List.map
@@ -189,11 +206,23 @@ let replace_lifting ~equality ~what ~with_what ~where =
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false
-    | C.Const _ as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-       C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t,
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+       in
+       C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,i,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+       in
+        C.MutInd (uri,i,exp_named_subst')
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+       in
+        C.MutConstruct (uri,i,j,exp_named_subst')
+    | C.MutCase (sp,i,outt,t,pl) ->
+       C.MutCase (sp,i,substaux k what outt, substaux k what t,
         List.map (substaux k what) pl)
     | C.Fix (i,fl) ->
        let len = List.length fl in
@@ -230,14 +259,20 @@ let reduce context =
          | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )
-    | C.Var uri as t ->
-       (match CicEnvironment.get_cooked_obj uri 0 with
-           C.Definition _ -> raise ReferenceToDefinition
-         | C.Axiom _ -> raise ReferenceToAxiom
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+       (match CicEnvironment.get_obj uri with
+           C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_) -> reduceaux context l body
+         | C.Variable (_,None,_,_) ->
+            let t' = C.Var (uri,exp_named_subst') in
+             if l = [] then t' else C.Appl (t'::l)
+         | C.Variable (_,Some body,_,_) ->
+            (reduceaux context l
+              (CicSubstitution.subst_vars exp_named_subst' body))
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
@@ -264,17 +299,36 @@ let reduce context =
        let tl' = List.map (reduceaux context []) tl in
         reduceaux context (tl'@l) he
     | C.Appl [] -> raise (Impossible 1)
-    | C.Const (uri,cookingsno) as t ->
-       (match CicEnvironment.get_cooked_obj uri cookingsno with
-           C.Definition (_,body,_,_) -> reduceaux context l body
-         | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
-         | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_) -> reduceaux context l body
-         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-       )
-    | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+        (match CicEnvironment.get_obj uri with
+            C.Constant (_,Some body,_,_) ->
+             (reduceaux context l
+               (CicSubstitution.subst_vars exp_named_subst' body))
+          | C.Constant (_,None,_,_) ->
+             let t' = C.Const (uri,exp_named_subst') in
+              if l = [] then t' else C.Appl (t'::l)
+          | C.Variable _ -> raise ReferenceToVariable
+          | C.CurrentProof (_,_,body,_,_) ->
+             (reduceaux context l
+               (CicSubstitution.subst_vars exp_named_subst' body))
+          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        )
+    | C.MutInd (uri,i,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       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 ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+        let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
+         if l = [] then t' else C.Appl (t'::l)
+    | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
@@ -307,30 +361,23 @@ let reduce context =
          | t -> t
        in
         (match decofix (reduceaux context [] term) with
-            C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
-          | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
-             let (arity, r, num_ingredients) =
+            C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
+          | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
+             let (arity, r) =
               match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,ingredients,r) ->
-                   let (_,_,arity,_) = List.nth tl i
-                   and num_ingredients =
-                    List.fold_right
-                     (fun (k,l) i ->
-                       if k < cookingsno then i + List.length l else i
-                     ) ingredients 0
-                   in
-                    (arity,r,num_ingredients)
+                 C.InductiveDefinition (tl,_,r) ->
+                   let (_,_,arity,_) = List.nth tl i in
+                    (arity,r)
                | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
-               let num_to_eat = r + num_ingredients in
-                let rec eat_first =
-                 function
-                    (0,l) -> l
-                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                  | _ -> raise (Impossible 5)
-                in
-                 eat_first (num_to_eat,tl)
+               let rec eat_first =
+                function
+                   (0,l) -> l
+                 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+                 | _ -> raise (Impossible 5)
+               in
+                eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
          | C.Cast _ | C.Implicit ->
@@ -340,7 +387,7 @@ let reduce context =
            let term' = reduceaux context [] term in
            let pl' = List.map (reduceaux context []) pl in
             let res =
-             C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+             C.MutCase (mutind,i,outtype',term',pl')
             in
              if l = [] then res else C.Appl (res::l)
        )
@@ -396,6 +443,8 @@ let reduce context =
           C.CoFix (i, fl')
         in
          if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;
@@ -438,15 +487,21 @@ let simpl context =
          | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )
-    | C.Var uri as t ->
-       (match CicEnvironment.get_cooked_obj uri 0 with
-           C.Definition _ -> raise ReferenceToDefinition
-         | C.Axiom _ -> raise ReferenceToAxiom
-         | C.CurrentProof _ -> raise ReferenceToCurrentProof
-         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_) -> reduceaux context l body
-       )
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+        (match CicEnvironment.get_obj uri with
+            C.Constant _ -> raise ReferenceToConstant
+          | C.CurrentProof _ -> raise ReferenceToCurrentProof
+          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+          | C.Variable (_,None,_,_) ->
+            let t' = C.Var (uri,exp_named_subst') in
+             if l = [] then t' else C.Appl (t'::l)
+          | C.Variable (_,Some body,_,_) ->
+             reduceaux context l
+              (CicSubstitution.subst_vars exp_named_subst' body)
+        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
     | C.Implicit as t -> t
@@ -472,88 +527,102 @@ let simpl context =
        let tl' = List.map (reduceaux context []) tl in
         reduceaux context (tl'@l) he
     | C.Appl [] -> raise (Impossible 1)
-    | C.Const (uri,cookingsno) as t ->
-       (match CicEnvironment.get_cooked_obj uri cookingsno with
-           C.Definition (_,body,_,_) ->
-            begin
-             try
-              (**** Step 2 ****)
-              let res,constant_args =
-               let rec aux rev_constant_args l =
-                function
-                   C.Lambda (name,s,t) as t' ->
-                    begin
-                     match l with
-                        [] -> raise WrongShape
-                      | he::tl ->
-                         (* when name is Anonimous the substitution should be *)
-                         (* superfluous                                       *)
-                         aux (he::rev_constant_args) tl (S.subst he t)
-                    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
-                     let (_,recindex,_,body) = List.nth fl i in
-                      let recparam =
-                       try
-                        List.nth l recindex
-                       with
-                        _ -> raise AlreadySimplified
-                      in
-                       (match CicReduction.whd context recparam with
-                           C.MutConstruct _
-                         | C.Appl ((C.MutConstruct _)::_) ->
-                            let body' =
-                             let counter = ref (List.length fl) in
-                              List.fold_right
-                               (function _ ->
-                                 decr counter ; S.subst (C.Fix (!counter,fl))
-                               ) fl body
-                            in
-                             (* Possible optimization: substituting whd *)
-                             (* recparam in l                           *)
-                             reduceaux (tys@context) l body',
-                              List.rev rev_constant_args
-                         | _ -> raise AlreadySimplified
-                       )
-                 | _ -> raise WrongShape
-               in
-                aux [] l body
-              in
-               (**** Step 3 ****)
-               let term_to_fold =
-                match constant_args with
-                   [] -> C.Const (uri,cookingsno)
-                 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+        (match CicEnvironment.get_obj uri with
+            C.Constant (_,Some body,_,_) ->
+             begin
+              try
+               (**** Step 2 ****)
+               let res,constant_args =
+                let rec aux rev_constant_args l =
+                 function
+                    C.Lambda (name,s,t) as t' ->
+                     begin
+                      match l with
+                         [] -> raise WrongShape
+                       | he::tl ->
+                          (* when name is Anonimous the substitution should *)
+                          (* be superfluous                                 *)
+                          aux (he::rev_constant_args) tl (S.subst he t)
+                     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
+                      let (_,recindex,_,body) = List.nth fl i in
+                       let recparam =
+                        try
+                         List.nth l recindex
+                        with
+                         _ -> raise AlreadySimplified
+                       in
+                        (match CicReduction.whd context recparam with
+                            C.MutConstruct _
+                          | C.Appl ((C.MutConstruct _)::_) ->
+                             let body' =
+                              let counter = ref (List.length fl) in
+                               List.fold_right
+                                (function _ ->
+                                  decr counter ; S.subst (C.Fix (!counter,fl))
+                                ) fl body
+                             in
+                              (* Possible optimization: substituting whd *)
+                              (* recparam in l                           *)
+                              reduceaux (tys@context) l body',
+                               List.rev rev_constant_args
+                          | _ -> raise AlreadySimplified
+                        )
+                  | _ -> raise WrongShape
+                in
+                 aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
                in
-                let reduced_term_to_fold = reduce context term_to_fold in
-                 replace (=) reduced_term_to_fold term_to_fold res
-             with
-                WrongShape ->
-                 (* The constant does not unfold to a Fix lambda-abstracted   *)
-                 (* w.r.t. zero or more variables. We just perform reduction. *)
-                 reduceaux context l body
-              | AlreadySimplified ->
-                 (* If we performed delta-reduction, we would find a Fix   *)
-                 (* not applied to a constructor. So, we refuse to perform *)
-                 (* delta-reduction.                                       *)
-                 if l = [] then
-                    t
-                 else
-                  C.Appl (t::l)
-            end
-         | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+                (**** Step 3 ****)
+                let term_to_fold =
+                 match constant_args with
+                    [] -> C.Const (uri,exp_named_subst')
+                  | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
+                in
+                 let reduced_term_to_fold = reduce context term_to_fold in
+                  replace (=) reduced_term_to_fold term_to_fold res
+              with
+                 WrongShape ->
+                  (* The constant does not unfold to a Fix lambda-abstracted  *)
+                  (* w.r.t. zero or more variables. We just perform reduction.*)
+                  reduceaux context l
+                   (CicSubstitution.subst_vars exp_named_subst' body)
+               | AlreadySimplified ->
+                  (* If we performed delta-reduction, we would find a Fix   *)
+                  (* not applied to a constructor. So, we refuse to perform *)
+                  (* delta-reduction.                                       *)
+                  let t' = C.Const (uri,exp_named_subst') in
+                   if l = [] then t' else C.Appl (t'::l)
+             end
+         | C.Constant (_,None,_,_) ->
+            let t' = C.Const (uri,exp_named_subst') in
+             if l = [] then t' else C.Appl (t'::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_) -> reduceaux context l body
+         | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
+    | C.MutInd (uri,i,exp_named_subst) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       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) ->
+       let exp_named_subst' =
+        reduceaux_exp_named_subst context l exp_named_subst
+       in
+        let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
+         if l = [] then t' else C.Appl (t'::l)
+    | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
@@ -584,30 +653,23 @@ let simpl context =
          | t -> t
        in
         (match decofix (reduceaux context [] term) with
-            C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
-          | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
-             let (arity, r, num_ingredients) =
+            C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
+          | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
+             let (arity, r) =
               match CicEnvironment.get_obj mutind with
                  C.InductiveDefinition (tl,ingredients,r) ->
-                   let (_,_,arity,_) = List.nth tl i
-                   and num_ingredients =
-                    List.fold_right
-                     (fun (k,l) i ->
-                       if k < cookingsno then i + List.length l else i
-                     ) ingredients 0
-                   in
-                    (arity,r,num_ingredients)
+                   let (_,_,arity,_) = List.nth tl i in
+                    (arity,r)
                | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
-               let num_to_eat = r + num_ingredients in
-                let rec eat_first =
-                 function
-                    (0,l) -> l
-                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                  | _ -> raise (Impossible 5)
-                in
-                 eat_first (num_to_eat,tl)
+               let rec eat_first =
+                function
+                   (0,l) -> l
+                 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+                 | _ -> raise (Impossible 5)
+               in
+                eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
          | C.Cast _ | C.Implicit ->
@@ -617,7 +679,7 @@ let simpl context =
            let term' = reduceaux context [] term in
            let pl' = List.map (reduceaux context []) pl in
             let res =
-             C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+             C.MutCase (mutind,i,outtype',term',pl')
             in
              if l = [] then res else C.Appl (res::l)
        )
@@ -673,6 +735,8 @@ let simpl context =
          C.CoFix (i, fl')
        in
          if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;