diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-13 12:54:02 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-13 13:56:29 -0500 |
| commit | 011e29790182b3c85889ce402f7fc9fad0ac0817 (patch) | |
| tree | df1d8950a3ea3b8b53e349193c7c312204d27858 /src | |
| parent | 4445906ebb0a224d9465634e37096b2a30d21109 (diff) | |
Reflow comment
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 645f81634..17f01e5d6 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -104,9 +104,9 @@ Declare Reduction interp_red not contain evars. Most tactics use [abstract] to reduce the load on [Defined] and to catch looping behavior early. *) -(** The tactic [unify_abstract_renamify_rhs_reflexivity] calls [renamify] on [RHS] and unifies - that with [LHS]; and then costs one [vm_compute] to prove the - equality. *) +(** The tactic [unify_abstract_renamify_rhs_reflexivity] calls + [renamify] on [RHS] and unifies that with [LHS]; and then costs + one [vm_compute] to prove the equality. *) Ltac unify_abstract_renamify_rhs_reflexivity := unify_transformed_rhs_abstract_tac ltac:(renamify) |