From ce2fd238ae65537f65067d402482adb1874176db Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 11:06:19 +0000 Subject: [PATCH] The outtype of the MutCase of the generated elimination principles are now always dependent (to avoid the ugly compatibility code with Coq). --- helm/ocaml/cic_proof_checking/cicElim.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) 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 -- 2.39.2