diff options
| author | Pierre-Marie Pédrot | 2015-03-23 13:10:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-23 13:10:34 +0100 |
| commit | 224d3b0e8be9b6af8194389141c9508504cf887c (patch) | |
| tree | e36a175c48d3b7c6bdd10eb9907f726af7f3a9e7 /proofs | |
| parent | 690ac9fe35ff153a2348b64984817cb37b7764e4 (diff) | |
| parent | 3646aea90ae927af9262e994048a3bd863c57839 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2917f52c58..5bff3c8131 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -295,7 +295,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let ctx = Evd.evar_universe_context_set universes in if keep_body_ucst_sepatate then (* For vi2vo compilation proofs are computed now but we need to - * completent the univ constraints of the typ with the ones of + * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) let ctx_body = restrict_universe_context ctx used_univs_body in let ctx_typ = restrict_universe_context ctx used_univs_typ in |