diff options
| author | barras | 2002-03-04 13:29:45 +0000 |
|---|---|---|
| committer | barras | 2002-03-04 13:29:45 +0000 |
| commit | 6274447373e7dc69234da3415f8d9c4d4b67ced2 (patch) | |
| tree | c2190c4f3ee24b87e49cec5927d02a77272ba42e /kernel/term.mli | |
| parent | 9935f0d7ab63d31f7a4a8c05d90627dff41dabf8 (diff) | |
Nouveau Rewrite-in plus economique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 00f835e0d5..73f29ddbe5 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -418,9 +418,6 @@ val liftn : int -> int -> constr -> constr (* [lift n c] lifts by [n] the positive indexes in [c] *) val lift : int -> constr -> constr -(* [pop c] lifts by -1 the positive indexes in [c] *) -val pop : constr -> constr - (* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [a1],...,[an] *) |