From 3e30c3516dbb98a0629eb0205085f3b79abe1469 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Oct 2004 12:18:22 +0000 Subject: [PATCH] ported to typed explicit subst --- helm/ocaml/cic_unification/cicRefine.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 7b3e4179c..dd510797a 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -159,12 +159,15 @@ and type_of_aux' metasenv context t = ty,subst',metasenv' | C.Meta (n,l) -> (try - let (canonical_context, term) = CicUtil.lookup_subst n subst in + let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in let subst,metasenv = check_metasenv_consistency n subst metasenv context canonical_context l in - type_of_aux subst metasenv context (CicSubstitution.lift_meta l term) + (* trust or check ??? *) + CicSubstitution.lift_meta l ty, subst, metasenv + (* type_of_aux subst metasenv + context (CicSubstitution.lift_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let subst,metasenv = -- 2.39.2