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 d91b00084012a6954e9b2b84b964ae61c251461d..777ccd5f5101b797f2cb92a48e53cb0c83bc2c7d 100644 (file)
--- 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