diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /pretyping/reductionops.ml | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 85e6f51387..2fc9dc2776 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -886,7 +886,7 @@ module CredNative = RedNative(CNativeEntries) (** Generic reduction function with environment Here is where unfolded constant are stored in order to be - eventualy refolded. + eventually refolded. If tactic_mode is true, it uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants @@ -1315,7 +1315,7 @@ let whd_allnolet_stack env = let whd_allnolet env = red_of_state_red (whd_allnolet_state env) -(* 4. Ad-hoc eta reduction, does not subsitute evars *) +(* 4. Ad-hoc eta reduction, does not substitute evars *) let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) |