Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 1 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0fb8d73740..89c4c84061 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -851,16 +851,20 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
       (true,pred) (* true = dependent -- par défaut *)
     else
+(*
       let s = get_sort_of env (evars_of isevars) typs.(0) in
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
       let predbody = mkMutCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
+*)
       (* "TODO4-2" *)
       error ("Unable to infer a Cases predicate\n"^
-"Either there is a type incompatiblity or the problem involves dependencies");
+"Either there is a type incompatiblity or the problem involves dependencies")
+(*
       (true,pred)
+*)
 
 (* Propagation of user-provided predicate through compilation steps *)