modification de la definition des def inductives unitaires et autorisation d'elimination sur la sorte Type

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

1 files changed, 26 insertions, 14 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4729598c76..12f1760407 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -132,9 +132,16 @@ let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
 let is_logic_arity infos =
   List.for_all (fun (logic,small) -> logic || small) infos
 
-let is_unit arinfos constrsinfos =
+(* An inductive definition is a "unit" if it has only one constructor
+   and that all arguments expected by this constructor are 
+   logical, this is the case for equality, conjonction of logical properties 
+*)
+let is_unit constrsinfos =
   match constrsinfos with  (* One info = One constructor *)
-   | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
+   | [constrinfos] -> is_logic_constr constrinfos 
+  (* CP : relax this constraint which was related 
+          to extraction 
+          && is_logic_arity arinfos *)
    | _ -> false
 
 let rec infos_and_sort env t =
@@ -148,10 +155,9 @@ let rec infos_and_sort env t =
     | Cast (c,_) -> infos_and_sort env c
     | _ -> []
 
-let small_unit constrsinfos (env_ar_par,short_arity) =
-  let issmall = List.for_all is_small constrsinfos in
-  let arinfos = infos_and_sort env_ar_par short_arity in
-  let isunit = is_unit arinfos constrsinfos in
+let small_unit constrsinfos =
+  let issmall = List.for_all is_small constrsinfos 
+  and isunit = is_unit constrsinfos in
   issmall, isunit
 
 (* This (re)computes informations relevant to extraction and the sort of an
@@ -178,7 +184,7 @@ let type_one_constructor env_ar_par params arsort c =
 
   (infos, full_cstr_type, cst2)
 
-let infer_constructor_packet env_ar params short_arity arsort vc =
+let infer_constructor_packet env_ar params arsort vc =
   let env_ar_par = push_rel_context params env_ar in
   let (constrsinfos,jlc,cst) = 
     List.fold_right
@@ -189,7 +195,7 @@ let infer_constructor_packet env_ar params short_arity arsort vc =
       vc
       ([],[],Constraint.empty) in
   let vc' = Array.of_list jlc in
-  let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
+  let issmall,isunit = small_unit constrsinfos in
   (issmall,isunit,vc', cst)
 
 (* Type-check an inductive definition. Does not check positivity
@@ -235,7 +241,7 @@ let type_inductive env mie =
 	 let (_,arsort) = dest_arity env full_arity in
 	 let lc = ind.mind_entry_lc in
 	 let (issmall,isunit,lc',cst') =
-	   infer_constructor_packet env_arities params short_arity arsort lc
+	   infer_constructor_packet env_arities params arsort lc
 	 in
 	 let nparams = ind.mind_entry_nparams in
 	 let consnames = ind.mind_entry_consnames in
@@ -249,15 +255,21 @@ let type_inductive env mie =
 
 (***********************************************************************)
 (***********************************************************************)
+let all_sorts = [InProp;InSet;InType]
+let impredicative_sorts = [InProp;InSet]
+let logical_sorts = [InProp]
 
 let allowed_sorts issmall isunit = function
-  | Type _ -> 
-      [InProp;InSet;InType]
+  | Type _ -> all_sorts
   | Prop Pos -> 
-      if issmall then [InProp;InSet;InType]
-      else [InProp;InSet]
+      if issmall then all_sorts
+      else impredicative_sorts
   | Prop Null -> 
-      if isunit then [InProp;InSet] else [InProp]
+(* Added InType which is derivable :when the type is unit and small *)
+      if isunit then 
+	if issmall then all_sorts
+	else impredicative_sorts
+      else logical_sorts
 
 type ill_formed_ind =
   | LocalNonPos of int