From 894a3d16471f19bd527730490ea242e218b62ff6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 26 Nov 2014 21:25:39 +0100
Subject: Fixing Coq compilation.

---
 pretyping/unification.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0af61d3a2..fa419ddaf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1008,6 +1008,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     let a = match res with 
     | Some sigma -> sigma, ms, es
     | None -> unirec_rec (env,0) cv_pb opt flags subst m n
+    in
     if !debug_unification then msg_debug (str "Leaving unification with success");
     a
   with e ->
-- 
cgit v1.2.3