From 47d4f5037926378d56b1a5050bd87415ed31d2dd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 23 May 2017 16:16:46 -0400
Subject: unification.mli: Fix a spelling typo in a comment

---
 pretyping/unification.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 148178f2fc..8d7e3521d6 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags
 
 val is_keyed_unification : unit -> bool
 
-(** The "unique" unification fonction *)
+(** The "unique" unification function *)
 val w_unify :
   env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
 
-- 
cgit v1.2.3