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 eecb0fae6a97826e037e8c150b14d3493a0d7c67..ab7ddd0e1fb2bb0a75bd4a4a48a3a82ae12f5f37 100644 (file)
--- 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