From e674cb67c1f52747111fa3935d1523e1af8222f5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 26 Nov 2005 18:05:10 +0000 Subject: [PATCH] * wrong comments removed * relocalization of refined terms is now performed for every refined term --- helm/ocaml/cic_unification/cicRefine.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 239db16cf..6d28ca177 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -207,7 +207,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - (* this stops on binders, so we have to call it every time *) + let (t',_,_,_,_) as res = match t with (* function *) C.Rel n -> @@ -392,7 +392,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in - relocalize localization_tbl x x'; (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in @@ -783,6 +782,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fl_ty' fl_bo' fl in C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 + in + relocalize localization_tbl t t'; + res (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - -- 2.39.2