From 8554834e58019a70f9a8755c5245fee293c39820 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Jul 2007 10:39:38 +0000 Subject: [PATCH] little bug in coercion generation found. it use to create more coercions that expected (luckily convertible). --- helm/software/components/tactics/closeCoercionGraph.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 2cff9c608..6c253df9f 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -25,7 +25,7 @@ (* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *) -let debug = false +let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* given the new coercion uri from src to tgt returns the list @@ -207,8 +207,10 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = let spline_len = saturations_for_c1 + saturations_for_c2 in let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); + let old_insert_coercions = !CicRefine.insert_coercions in let c, metasenv, univ = try + CicRefine.insert_coercions := false; let term, ty, metasenv, ugraph = CicRefine.type_of_aux' metasenv context c univ in @@ -251,11 +253,16 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = in debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term)); debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); + CicRefine.insert_coercions := old_insert_coercions; term, metasenv, ugraph with | CicRefine.RefineFailure s | CicRefine.Uncertain s -> debug_print s; + CicRefine.insert_coercions := old_insert_coercions; raise UnableToCompose + | exn -> + CicRefine.insert_coercions := old_insert_coercions; + raise exn in c, metasenv, univ ;; -- 2.39.2