X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=e7b0e3661387d3b986a292858962532f9c4588a5;hb=45b8f3d3fcc007ffd2e7891b992444908aa1a2fd;hp=4ee37168450dc9fc84c409a82a40d9ef25828140;hpb=c17dc580374628504e9c7fac7f59bd7ddf7d420e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 4ee371684..e7b0e3661 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -1,8 +1,33 @@
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
 
 open Printf
 
-exception AssertFailure of string
 exception MetaSubstFailure of string
+exception Uncertain of string
+exception AssertFailure of string
 
 let debug_print = prerr_endline
 
@@ -27,7 +52,7 @@ let apply_subst_gen ~appl_fun subst term =
           in
            C.Meta (i,l'))
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
@@ -280,7 +305,7 @@ let rec force_does_not_occur subst to_be_restricted t =
       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
     | C.Rel _
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Meta (n, l) ->
        (* we do not retrieve the term associated to ?n in subst since *)
        (* in this way we can restrict if something goes wrong         *)
@@ -516,7 +541,7 @@ let delift n subst context metasenv l t =
            let l' = deliftl 1 l1 in
             C.Meta(i,l')
      | C.Sort _ as t -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
@@ -567,8 +592,9 @@ let delift n subst context metasenv l t =
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-      raise (MetaSubstFailure (sprintf
+debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
+print_string "\nCicMetaSubst: UNCERTAIN" ;
+      raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "