diff options
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 |