diff options
| author | herbelin | 2006-05-23 16:11:31 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-23 16:11:31 +0000 |
| commit | 1ab5ab37724864b1d4fbe1ad4777b24093235270 (patch) | |
| tree | 5c6a8377aa6dc806a2ec9b488508a1f43714eca2 /kernel | |
| parent | bab93b9eda03f1ca13e7ff2a0b83bf43eea1874b (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 1 |
2 files changed, 2 insertions, 0 deletions
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 |