From 599746792b5faba523a11f25d04992ddf34f87f3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 17 Dec 2003 17:37:03 +0000 Subject: [PATCH] More comments. Some of them may highlight bugs or open issues. --- helm/ocaml/cic_unification/cicUnification.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index bc736b260..e0d4d13f2 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -77,11 +77,17 @@ let delift context metasenv l t = if m <=k then C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) (*CSC: deliftato la regola per il LetIn *) + (*CSC: FALSO! La regola per il LetIn non lo fa *) else (match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t) + Some (_,C.Def (t,_)) -> + (*CSC: Hmmm. This bit of reduction is not in the spirit of *) + (*CSC: first order unification. Does it help or does it harm? *) + deliftaux k (S.lift m t) | Some (_,C.Decl t) -> (* It may augment to_be_restricted *) + (*CSC: Really? Even in the case of well-typed terms? *) + (*CSC: I am no longer sure of the usefulness of the check *) ignore (deliftaux k (S.lift m t)) ; C.Rel ((position (m-k) l) + k) | None -> raise RelToHiddenHypothesis) -- 2.39.2