diff options
| author | Hugo Herbelin | 2015-10-13 11:40:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-18 20:11:14 +0200 |
| commit | c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff (patch) | |
| tree | 2db781cc2a505a805fc53abac8d422b1192aef1e /proofs | |
| parent | c70ee60ed1603658eb33f4ae39b1a0be81bf45c6 (diff) | |
Miscellaneous typos, spacing, US spelling in comments or variable names.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic_monad.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index 81f02b66db..b9165aa812 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -188,7 +188,7 @@ struct shape of the monadic type is reminiscent of that of the continuation monad transformer. - The paper also contains the rational for the [split] abstraction. + The paper also contains the rationale for the [split] abstraction. An explanation of how to derive such a monad from mathematical principles can be found in "Kan Extensions for Program diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 028116049c..fcb706cc8d 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -94,7 +94,7 @@ val start_dependent_proof : val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. - * Both access the current proof state. The formes is supposed to be + * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context |