From c6e628b75a549ade8b1133fdea9101f49ca4f991 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 17 Mar 2015 18:32:52 +0100
Subject: typo

---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3