From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 28 May 2009 18:15:13 +0000 (+0000)
Subject: Procedural: higher-order unification needs a lot of hints !!
X-Git-Tag: make_still_working~3939
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6daa2cc113783aaba53d82c47fe7107988d76e11;p=helm.git

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
---

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