module Wcclausenv

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

5 files changed, 25 insertions, 17 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 429d626f1f..0154aa7a96 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -50,6 +50,19 @@ let mis_recargs mis =
 let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
 
+let is_recursive listind = 
+  let rec one_is_rec rvec = 
+    List.exists (function
+		   | Mrec(i)        -> List.mem i listind 
+                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Norec          -> false
+                   | Param(_)       -> false) rvec
+  in 
+  array_exists one_is_rec
+
+let mis_is_recursive mis =
+  is_recursive (interval 0 ((mis_ntypes mis)-1)) (mis_recarg mis)
+
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
 (*s Declaration. *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 46c781eea0..d9a11fe478 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -56,6 +56,7 @@ val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
+val mis_is_recursive : mind_specif -> bool
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 93243a4404..1a1ea5bbb4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -42,7 +42,7 @@ let stack_reduction_of_reduction red_fun env sigma x stack =
   whd_stack env sigma t []
 
 let strong whdfun env sigma = 
-  let rec strongrec = function
+  let rec strongrec t = match whdfun env sigma t with
     | DOP0 _ as t -> t
     (* Cas ad hoc *)
     | DOP1(oper,c) -> DOP1(oper,strongrec c)
@@ -914,8 +914,8 @@ and eqappr cv_pb infos appr1 appr2 =
 
 
 let fconv cv_pb env sigma t1 t2 =
-  let t1 = strong (fun _ -> strip_outer_cast) env sigma t1
-  and t2 = strong (fun _ -> strip_outer_cast) env sigma t2 in
+  let t1 = strong (fun _ _ -> strip_outer_cast) env sigma t1
+  and t2 = strong (fun _ _ -> strip_outer_cast) env sigma t2 in
   if eq_constr t1 t2 then 
     Constraint.empty
   else
@@ -948,8 +948,8 @@ let is_conv_leq env sigma = test_conversion conv_leq env sigma
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta env sigma = function
-  | DOP0(Meta p) as u -> (try List.assoc p (metamap sigma) with Not_found -> u)
+let whd_meta metamap = function
+  | DOP0(Meta p) as u -> (try List.assoc p metamap with Not_found -> u)
   | x -> x
 	
 (* Try to replace all metas. Does not replace metas in the metas' values
@@ -1300,7 +1300,7 @@ let rec whd_ise1 env sigma = function
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
-let nf_ise1 env sigma = strong (whd_ise1 env sigma) env sigma
+let nf_ise1 env sigma = strong whd_ise1 env sigma
 
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 585a573449..1ff259e01a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -177,7 +177,7 @@ val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
 
 (*s Special-Purpose Reduction Functions *)
 
-val whd_meta : 'a reduction_function
+val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> 'a reduction_function
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 5113612413..5f8cfefc01 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -172,10 +172,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
       [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
       [bodies   = [b1,.....bn]]
-   then 
-
-   [ mkFix recindxs i typarray funnames bodies]
-   
+   then [ mkFix recindxs i typarray funnames bodies]
    constructs the $i$th function of the block  
 
     [Fixpoint f1 [ctx1] = b1
@@ -183,7 +180,7 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
      ...
      with     fn [ctxn] = bn.]
 
-   where the lenght of the $j$th context is $ij$.
+   \noindent where the lenght of the $j$th context is $ij$.
 *)
 val mkFix : int array -> int -> typed_type array -> name list 
   -> constr array -> constr
@@ -194,11 +191,8 @@ val mkFixDlam : int array -> int -> typed_type array
 
 (* If [typarray = [|t1,...tn|]]
       [funnames = [f1,.....fn]]
-      [bodies   = [b1,.....bn]]
-   then
-
-      [mkCoFix i typsarray funnames bodies]
-
+      [bodies   = [b1,.....bn]] \par\noindent
+   then [mkCoFix i typsarray funnames bodies]
    constructs the ith function of the block  
    
     [CoFixpoint f1 = b1