diff options
| author | barras | 2001-03-23 15:04:09 +0000 |
|---|---|---|
| committer | barras | 2001-03-23 15:04:09 +0000 |
| commit | fae106f740d3d71555933cf416eec905c58f417e (patch) | |
| tree | 12cfd6fa08b20e9f076c113a1a668388c5cf5527 /pretyping | |
| parent | fab1cc89b9ff65938cff3b4e41e51ad3b0bc68db (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |