From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 Jul 2005 11:06:19 +0000 (+0000)
Subject: The outtype of the MutCase of the generated elimination principles are now
X-Git-Tag: pre_notation~52
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ce2fd238ae65537f65067d402482adb1874176db;p=helm.git

The outtype of the MutCase of the generated elimination principles are now
always dependent (to avoid the ugly compatibility code with Coq).
---

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index eecb0fae6..ab7ddd0e1 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -319,9 +319,23 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
               (shift + 1,  b :: branches))
             constructors (1, [])
         in
+        let shiftno  = conslen + rightno + 2 + recshift in
+        let outtype =
+         if dependent then
+          Cic.Rel shiftno
+         else
+          let head =
+           if rightno = 0 then
+            CicSubstitution.lift 1 (Cic.Rel shiftno)
+           else
+            Cic.Appl
+             ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) ::
+              mk_rels 1 rightno)
+          in
+           add_right_lambda true leftno shiftno 1 rightno indty head ty
+        in
         let mutcase =
-          Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 2 + recshift),
-            Cic.Rel 1, branches)
+          Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches)
         in
         let body =
           if is_recursive then