...

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 98b06f94e689d5d138d610eb130809512f8e2f78..147bb555fe349a063c9f6fc77cb52e7993d6bd56 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -39,34 +39,26 @@ let flexible l =
 
 exception WrongShape;;
 
-let eta_reduce after_beta_expansion after_beta_expansion_body
-     before_beta_expansion
- =
- try
-  match before_beta_expansion,after_beta_expansion_body with
-  | NCic.Appl l1, NCic.Appl l2 ->
-      NCicUtils.does_not_occur 0 1 (NCic.Appl (List.tail (List.rev l2)))
-      ...
-      let rec all_but_last check_last = function
-        | [] -> assert false
-        | [NCic.Rel 1] -> []
-        | [_] -> if check_last then raise WrongShape else []
-        | he::tl -> he::(all_but_last check_last tl)
-      in
-      let all_but_last check_last l =
-        match all_but_last check_last l with
-        | [] -> assert false
-        | [he] -> he
-        | l -> NCic.Appl l
-      in
-      let impossible_term = NCic.Rel ~-1 in
-      let t = NCicSubstitution.subst impossible_term (all_but_last true l2) in
-      let all_but_last = all_but_last false l1 in
-      if t = all_but_last then all_but_last else after_beta_expansion
-  | _ -> after_beta_expansion
- with WrongShape -> after_beta_expansion
+let eta_reduce = 
+  let delift_if_not_occur body orig =
+    try 
+        NCicSubstitution.psubst ~avoid_beta_redexes:true
+          (fun () -> raise WrongShape) [()] body
+    with WrongShape -> orig
+  in
+  function
+  | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig ->
+      delift_if_not_occur hd orig
+  | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig
+    when HExtlib.list_last l = NCic.Rel 1 ->
+       let body = 
+         let args, _ = Hextlib.split_nth (List.length l - 1) l in
+         NCic.Appl (hd::args)
+       in
+       delift_if_not_occur body orig
+  | t -> t
 ;;
-
+  
 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
@@ -100,8 +92,12 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   let fresh_name = "Hbeta" ^ string_of_int num in
   let (metasenv,subst,_), t1 = 
     aux (0, context, test_eq_only) (metasenv, subst) t in
-  let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) t1 t in
-  metasenv, subst, t2
+  let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in
+  try 
+    ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
+    metasenv, subst, t2
+  with NCicTypeChecker.TypeCheckerFailure _ -> 
+    NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
   let _, subst, metasenv, hd =