diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-10 04:54:35 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-27 14:02:32 +0200 |
| commit | 70e87f6e67198b1340dfffe1e2a7d741706125f9 (patch) | |
| tree | acd4ffd72add93d3dc70363dce1b82c9c1db82c9 /engine/termops.mli | |
| parent | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (diff) | |
Fix documentation.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 4581e2310..6c680005d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -134,7 +134,7 @@ val pop : constr -> constr (** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -(** [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq] +(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) val subst_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr @@ -145,7 +145,7 @@ val replace_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr -> constr -(** [subst_term d c] replaces [Rel 1] by [d] in [c] *) +(** [subst_term d c] replaces [d] by [Rel 1] in [c] *) val subst_term : constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) |