]> matita.cs.unibo.it Git - helm.git/commitdiff
Now it compiles again.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Dec 2008 20:32:15 +0000 (20:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Dec 2008 20:32:15 +0000 (20:32 +0000)
helm/software/components/cic_unification/cicRefine.ml

index ad4d0106539f9c207a7e91ebba1d7bf1ebe72f5b..cf7e582e611a6eb54d842243d5d372406db2c52b 100644 (file)
@@ -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 *)