From 1ab5ab37724864b1d4fbe1ad4777b24093235270 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2006 16:11:31 +0000
Subject: Ajout substl_named_decl pour mode Maple

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml  | 1 +
 kernel/term.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index f59a6c1834..af0f2e4b8d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -779,6 +779,7 @@ let substnl_decl laml k (id,bodyopt,typ) =
 let substl_decl laml = substnl_decl laml 0
 let subst1_decl lam = substl_decl [lam]
 let subst1_named_decl = subst1_decl
+let substl_named_decl = substl_decl
 
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 0982ee4569..78802579a3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -465,6 +465,7 @@ val substl_decl : constr list -> rel_declaration -> rel_declaration
 val subst1_decl : constr -> rel_declaration -> rel_declaration
 
 val subst1_named_decl : constr -> named_declaration -> named_declaration
+val substl_named_decl : constr list -> named_declaration -> named_declaration
 
 val replace_vars : (identifier * constr) list -> constr -> constr
 val subst_var : identifier -> constr -> constr
-- 
cgit v1.2.3