From 4d00de7ac4ad9d35feb88b605d099f729490ba35 Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 28 Feb 2001 15:49:58 +0000
Subject: Changement de subst_meta

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 43a671536c..18e3d2c324 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -840,6 +840,13 @@ let fconv cv_pb env sigma t1 t2 =
 let conv env = fconv CONV env
 let conv_leq env = fconv CONV_LEQ env 
 
+let convleqkey = Profile.declare_profile "conv_leq";;
+let conv_leq env sigma t1 t2 = Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
+
+
+let convkey = Profile.declare_profile "conv";;
+let conv env sigma t1 t2 = Profile.profile4 convleqkey conv env sigma t1 t2;;
+
 let conv_forall2 f env sigma v1 v2 =
   array_fold_left2 
     (fun c x y -> let c' = f env sigma x y in Constraint.union c c')
-- 
cgit v1.2.3