From a27ac0315dcbb99c64a260bac3988199a26b39cf Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 24 Nov 2016 15:14:19 +0100 Subject: Fix some documentation typos. Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. --- CHANGES | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 984e91946b..ecbf82e69d 100644 --- a/CHANGES +++ b/CHANGES @@ -1130,7 +1130,7 @@ Extraction instead of accessing their body, they are now considered as axioms. The previous behaviour can be reactivated via the option "Set Extraction AccessOpaque". -- The pretty-printer for Haskell now produces layout-independant code +- The pretty-printer for Haskell now produces layout-independent code - A new command "Separate Extraction cst1 cst2 ..." that mixes a minimal extracted environment a la "Recursive Extraction" and the production of several files (one per coq source) a la "Extraction Library" @@ -1815,7 +1815,7 @@ Tactics Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used - independantly of romega. + independently of romega. - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an -- cgit v1.2.3