From fc2a7e960567bd6134679dda157ffc8af8b4ea75 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 24 Apr 2007 13:42:00 +0000 Subject: [PATCH] @ --- components/cic_unification/cicMetaSubst.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index a86bc471a..a361b7a32 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -338,9 +338,10 @@ let ppcontext' ~metasenv ?(sep = "\n") subst context = let ppsubst_unfolded ~metasenv subst = String.concat "\n" (List.map - (fun (idx, (c, t,_)) -> + (fun (idx, (c, t,ty)) -> let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d:= %s" context idx + sprintf "%s |- ?%d : %s := %s" context idx +(ppterm_in_name_context ~metasenv [] ty name_context) (ppterm_in_name_context ~metasenv subst t name_context)) subst) (* @@ -351,9 +352,9 @@ let ppsubst_unfolded ~metasenv subst = let ppsubst ~metasenv subst = String.concat "\n" (List.map - (fun (idx, (c, t, _)) -> + (fun (idx, (c, t, ty)) -> let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in - sprintf "%s |- ?%d:= %s" context idx + sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context) (ppterm_in_name_context ~metasenv [] t name_context)) subst) ;; @@ -640,7 +641,7 @@ let delift n subst context metasenv l t = if m <=k then C.Rel m else - (try + (try match List.nth context (m-k-1) with Some (_,C.Def (t,_)) -> (*CSC: Hmmm. This bit of reduction is not in the spirit of *) @@ -654,7 +655,7 @@ let delift n subst context metasenv l t = C.Rel ((position (m-k) l) + k) | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) with - Failure _ -> + Failure _ -> raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) ) | C.Var (uri,exp_named_subst) -> -- 2.39.2