portage modules Evarconv et Evarutil

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

4 files changed, 19 insertions, 12 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5f011c06d..4bc551c6a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -933,7 +933,7 @@ let test_conversion f env sigma x y =
 
 let is_conv env sigma = test_conversion conv env sigma
 let is_conv_leq env sigma = test_conversion conv_leq env sigma
-
+let is_fconv = function | CONV -> is_conv | CONV_LEQ -> is_conv_leq
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
@@ -1268,30 +1268,30 @@ let poly_args env sigma t =
 
 exception Uninstantiated_evar of int
 
-let rec whd_ise env sigma = function
+let rec whd_ise sigma = function
   | DOPN(Evar sp,_) as k ->
       if Evd.in_dom sigma sp then
         if Evd.is_defined sigma sp then
-          whd_ise env sigma (existential_value sigma k)
+          whd_ise sigma (existential_value sigma k)
         else raise (Uninstantiated_evar sp)
       else k
-  | DOP2(Cast,c,_) -> whd_ise env sigma c
+  | DOP2(Cast,c,_) -> whd_ise sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
 
 (* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 env sigma = function
+let rec whd_ise1 sigma = function
   | (DOPN(Evar sp,_) as k) ->
       if Evd.in_dom sigma sp & Evd.is_defined sigma sp then
-        whd_ise1 env sigma (existential_value sigma k)
+        whd_ise1 sigma (existential_value sigma k)
       else 
 	k
-  | DOP2(Cast,c,_) -> whd_ise1 env sigma c
+  | DOP2(Cast,c,_) -> whd_ise1 sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
-let nf_ise1 env sigma = strong whd_ise1 env sigma
+let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_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 3e2fc9ffd..9945b36cb 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -172,6 +172,7 @@ val conv_forall2_i :
 
 val is_conv : unsafe_env -> 'a evar_map -> constr -> constr -> bool
 val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
+val is_fconv : conv_pb -> unsafe_env -> 'a evar_map -> constr -> constr -> bool
 
 
 (*s Special-Purpose Reduction Functions *)
@@ -182,11 +183,13 @@ val instance : (int * constr) list -> 'a reduction_function
 
 (* whd_ise raise Uninstantiated_evar if an evar remains uninstantiated *)
 (* the '*_ise1*' leave uninstantiated evar as it *)
+
 exception Uninstantiated_evar of int
-val whd_ise : 'a reduction_function
-val whd_ise1 : 'a reduction_function
-val nf_ise1 : 'a reduction_function
-val whd_ise1_metas : 'a reduction_function
+
+val whd_ise : 'a evar_map -> constr -> constr
+val whd_ise1 : 'a evar_map -> constr -> constr
+val nf_ise1 : 'a evar_map -> constr -> constr
+val whd_ise1_metas : 'a evar_map -> constr -> constr
 
 
 (*s Obsolete Reduction Functions *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index eaef2dafc..f3cb78205 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -29,6 +29,8 @@ type type_error =
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
+  | OccurCheck of int * constr
+  | NotClean of int * constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 23fed99f3..a3820217b 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -31,6 +31,8 @@ type type_error =
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
+  | OccurCheck of int * constr
+  | NotClean of int * constr
 
 exception TypeError of path_kind * context * type_error