diff options
| author | mohring | 2001-02-28 15:49:58 +0000 |
|---|---|---|
| committer | mohring | 2001-02-28 15:49:58 +0000 |
| commit | 4d00de7ac4ad9d35feb88b605d099f729490ba35 (patch) | |
| tree | 0b0e620772609f9f3ca4dccbd7dbf9ad95bda963 /kernel/term.ml | |
| parent | e5e6d2c234e885ba814b67b0421dca3f57659208 (diff) | |
Changement de subst_meta
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index f942fe1787..d75bea0087 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -940,6 +940,11 @@ let substn_many lamv n = in substrec n +(* +let substkey = Profile.declare_profile "substn_many";; +let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +*) + let substnl laml k = substn_many (Array.map make_substituend (Array.of_list laml)) k let substl laml = @@ -973,6 +978,11 @@ let replace_vars var_alist = in if var_alist = [] then (function x -> x) else substrec 0 +(* +let repvarkey = Profile.declare_profile "replace_vars";; +let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; +*) + (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) let subst_var str = replace_vars [(str, mkRel 1)] @@ -1561,7 +1571,7 @@ let subst_term_eta = subst_term_gen eta_eq_constr (* Et puis meta doit fusionner avec Evar *) let rec subst_meta bl c = match kind_of_term c with - | IsMeta i -> List.assoc i bl + | IsMeta i -> (try List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c (* Substitute only a list of locations locs, the empty list is |