From 988c82d4f12d40605db40212d396d9bc7f6b5eb6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Dec 2003 13:17:51 +0000 Subject: [PATCH] Big bug spotted: restriction can fail and it was implicitly assumed that it didn't. Added another comment in the code. --- helm/ocaml/cic_unification/cicUnification.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index d50818f73..8ba84c74c 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -52,6 +52,12 @@ let position n = aux 1 ;; +(*CSC: this restriction function is utterly wrong, since it does not check *) +(*CSC: that the variable that is going to be restricted does not occur free *) +(*CSC: in a part of the sequent that is not going to be restricted. *) +(*CSC: In particular, the whole approach is wrong; if restriction can fail *) +(*CSC: (as indeed it is the case), we can not collect all the restrictions *) +(*CSC: and restrict everything at the end ;-( *) let restrict to_be_restricted = let rec erase i n = function -- 2.39.2