diff options
| author | Pierre-Marie Pédrot | 2021-03-06 23:32:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-12 13:39:03 +0100 |
| commit | 285419e99996354ad2056bc38725c7a592124e7c (patch) | |
| tree | e4501ef5d6ccfa34643fde049e98fd156830bf54 /engine/termops.mli | |
| parent | 93ea9206cbf29617feb23646f95e794b11e87793 (diff) | |
Further simplification of the term replacing code.
We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index bfdb3fbc40..bdde2c450d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -122,16 +122,12 @@ val pop : constr -> constr (** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] - as equality *) -val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> int * constr -> constr -> bool) -> constr -> constr -> constr - -(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] - as equality *) +(** [replace_term_gen eq arity e c] replaces matching subterms according to + [eq] by [e] in [c]. If [arity] is non-zero applications of larger length + are handled atomically. *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> int * constr -> constr -> bool) -> - constr -> constr -> constr -> constr + Evd.evar_map -> (Evd.evar_map -> int -> constr -> bool) -> + int -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) val subst_term : Evd.evar_map -> constr -> constr -> constr |