From 32e29e1be132c4f9453787a194314ed57aa18538 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jun 2007 08:35:33 +0000 Subject: [PATCH] compose now returns a good metasenv --- helm/software/components/tactics/closeCoercionGraph.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 3e6411098..898946ad6 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -77,7 +77,6 @@ exception UnableToCompose (* generate_composite (c2 (c1 s)) in the universe graph univ * both living in the same context and metasenv *) let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = - let module RT = RefinementTool in let original_metasenv = metasenv in let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in @@ -106,7 +105,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = in let compose c1 nc1 c2 nc2 = Cic.Lambda - (Cic.Name "x", (Cic.Implicit None), + (Cic.Name "x", (Cic.Implicit (Some `Type)), (Cic.Appl ( CicSubstitution.lift 1 c2 :: mk_implicits nc2 @ [ Cic.Appl ( CicSubstitution.lift 1 c1 :: mk_implicits nc1 @ [if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None]) @@ -229,6 +228,12 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = let body_metasenv, lambdas_metasenv = split_metasenv metasenv (spline_len + List.length context) in + let lambdas_metasenv = + List.filter + (fun (i,_,_) -> + List.for_all (fun (j,_,_) -> i <> j) original_metasenv) + lambdas_metasenv + in let term = purge_unused_lambdas lambdas_metasenv term in let metasenv = List.filter -- 2.39.2