X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=96b38e424970161afcbd301424eee55079f4adee;hb=cdb9c1c0efcf68e15f0d7e63f5d92dc87d2b3ac9;hp=bd6eca4a51a377ac95096ae4a27c10516d0efa3b;hpb=34dfcf625e3ee6fac4ad4f7199055dee4edc5abb;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index bd6eca4a5..96b38e424 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         *)
@@ -485,16 +510,6 @@ let delift n subst context metasenv l t =
              (*CSC: first order unification. Does it help or does it harm? *)
              deliftaux k (S.lift m t)
           | Some (_,C.Decl t) ->
-             (*CSC: The following check seems to be wrong!             *)
-             (*CSC: B:Set |- ?2 : Set                                  *)
-             (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x                 *)
-             (*CSC: Why should I restrict ?2 over B? The instantiation *)
-             (*CSC: ?1 := A is perfectly reasonable and well-typed.    *)
-             (*CSC: Thus I comment out the following two lines that    *)
-             (*CSC: are the incriminated ones.                         *)
-             (*(* It may augment to_be_restricted *)
-               ignore (deliftaux k (S.lift m t)) ;*)
-             (*CSC: end of bug commented out                           *)
              C.Rel ((position (m-k) l) + k)
           | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
      | C.Var (uri,exp_named_subst) ->
@@ -526,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)
@@ -577,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_endline "\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 "; "