From 6274447373e7dc69234da3415f8d9c4d4b67ced2 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 4 Mar 2002 13:29:45 +0000
Subject: Nouveau Rewrite-in plus economique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml  | 2 ++
 pretyping/termops.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 867bbf50f1..11afda96bc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -331,6 +331,8 @@ let dependent m t =
   in 
   try deprec m t; false with Occur -> true
 
+let pop t = lift (-1) t
+
 (***************************)
 (*  substitution functions *)                         
 (***************************)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1bb74a3038..c45b1b016c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -76,6 +76,9 @@ val subst_meta : (int * constr) list -> constr -> constr
 val whd_locals : env -> constr -> constr
 val nf_locals  : env -> constr -> constr
 
+(* [pop c] lifts by -1 the positive indexes in [c] *)
+val pop : constr -> constr
+
 (* substitution of an arbitrary large term. Uses equality modulo
    reduction of let *)
 val dependent : constr -> constr -> bool
-- 
cgit v1.2.3