From fbdbbd2cea72f5f2d9d677ca466ceed63d969e33 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 14 May 2004 15:43:01 +0000
Subject: test de conversion laissait echapper exception NotConvertible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.mli | 17 -----------------
 1 file changed, 17 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d2f260b7b0..2a76441ad1 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -169,23 +169,6 @@ val pb_equal : conv_pb -> conv_pb
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
 val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
 
-type  conversion_function = 
-    env ->  evar_map -> constr -> constr -> constraints
-
-(* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
-   [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
-
-val conv :  conversion_function
-val conv_leq :  conversion_function
-
-val conv_forall2 : 
-   conversion_function -> env ->  evar_map -> constr array 
-    -> constr array -> constraints
-
-val conv_forall2_i : 
-  (int ->  conversion_function) -> env ->  evar_map
-    -> constr array -> constr array -> constraints
-
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
 val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
-- 
cgit v1.2.3