From fae106f740d3d71555933cf416eec905c58f417e Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 23 Mar 2001 15:04:09 +0000
Subject: amelioration de la consommation memoire de la conversion en
 eta-expansant les definitions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7a1423c3c9..a891cdd039 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -20,7 +20,6 @@ open Classops
 open Recordops 
 open Evarutil
 
-
 type flexible_term = FConst of constant | FRel of int | FVar of identifier 
 type flex_kind_of_term =
   | Rigid of constr 
@@ -314,6 +313,6 @@ and check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
-let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV     t1 t2
-let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CONV_LEQ t1 t2
+let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV  t1 t2
+let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
  
-- 
cgit v1.2.3