From 30641ee6278838b8b2a0b567d61f8f143582a217 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Dec 2008 20:32:15 +0000
Subject: [PATCH] Now it compiles again.

---
 helm/software/components/cic_unification/cicRefine.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index ad4d01065..cf7e582e6 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1979,7 +1979,7 @@ let typecheck metasenv uri obj ~localization_tbl =
       (match CicReduction.whd [] ty' with
           Cic.Sort _
         | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
-        | _ -> raise (RefineFailure (lazy ""))
+        | _ -> raise (RefineFailure (lazy "")))
   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
      assert (metasenv' = metasenv);
      (* Here we do not check the metasenv for correctness *)
-- 
2.39.2