From 6daa2cc113783aaba53d82c47fe7107988d76e11 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 May 2009 18:15:13 +0000 Subject: [PATCH] Procedural: higher-order unification needs a lot of hints !! files fully reconstructed today: nat/lt_arith.ma nat/div_and_mod.ma Z/plus.ma Z/orders.ma --- helm/software/components/acic_procedural/procedural2.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index d91b00084..777ccd5f5 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -194,11 +194,9 @@ let mk_exp_args hd tl classes synth qs = let exp = ref 0 in let meta id = C.AImplicit (id, None) in let map v (cl, b) = - if I.overlaps synth cl then - let w = if H.is_atomic (H.cic v) then v else meta "" in - if b then v, v else meta "", w - else - meta "", meta "" + if I.overlaps synth cl + then if b then v, v else meta "", v + else meta "", meta "" in let rec rev a = function | [] -> a -- 2.39.2