diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
| commit | c7dcb76ffff6b12b031e906b002b4d76c1aaea50 (patch) | |
| tree | 8d5115258c3b7042767e45d742e2800dab209822 /proofs/proof_global.mli | |
| parent | 666568377cbe1c18ce479d32f6359aa61af6d553 (diff) | |
| parent | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a11c7b4e0..929bb86e8 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -97,7 +97,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 |