From 2d23138f12504ba92274f91a5ced014e1a20511e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 26 Nov 2005 16:23:34 +0000 Subject: [PATCH] Bug fixed: an unrefined term was passed around while checking explicit named substitutions. --- helm/ocaml/cic_unification/cicRefine.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index ccf662f18..2b4b68947 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -849,9 +849,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = match tl with [] -> [],metasubst,metasenv,ugraph - | ((uri,t) as subst)::tl -> + | (uri,t)::tl -> let ty_uri,ugraph1 = type_of_variable uri ugraph in let typeofvar = +prerr_endline ("<<<" ^ CicPp.ppterm ty_uri); CicSubstitution.subst_vars substs ty_uri in (* CSC: why was this code here? it is wrong (match CicEnvironment.get_cooked_obj ~trust:false uri with @@ -867,8 +868,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ) ; *) let t',typeoft,metasubst',metasenv',ugraph2 = - type_of_aux metasubst metasenv context t ugraph1 - in + type_of_aux metasubst metasenv context t ugraph1 in + let subst = uri,t' in let metasubst'',metasenv'',ugraph3 = try fo_unif_subst -- 2.39.2