diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-17 18:32:52 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-22 12:08:03 +0100 |
| commit | c6e628b75a549ade8b1133fdea9101f49ca4f991 (patch) | |
| tree | ca211c5f52298b4ce5271e8b4543ad98452ff127 /proofs | |
| parent | c2d165e1ccfde9166b262b3fbcd9c648aef26528 (diff) | |
typo
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 2917f52c5..5bff3c813 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 |