From e1a0d19ddcb2682947ef610f8634cc80c134b558 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Oct 2009 17:55:03 +0000 Subject: [PATCH] hints input is cleared from projection redexes --- .../components/ng_refiner/nCicUnification.ml | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 7395aa7ac..b91585fbe 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -611,11 +611,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = in let try_hints metasenv subst t1 t2 (* exc*) = (*D*) inside 'H'; try let rc = -(* - prerr_endline ("\nProblema:\n" ^ + pp(lazy ("\nProblema:\n" ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2); -*) + NCicPp.ppterm ~metasenv ~subst ~context t2)); let candidates = NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2 in @@ -643,6 +641,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = unify rdb test_eq_only metasenv subst context x y) (metasenv, subst) premises in + pp(lazy("FUNZIONA!")); Some (metasenv, subst) (*D*) in outside true; rc with exn -> outside false; raise exn with @@ -731,12 +730,20 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn) | Uncertain msg as exn -> - match try_hints metasenv subst t1 t2 with +(* + prerr_endline "PROBLEMA"; + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1); + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2); +*) + let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in + match + try_hints metasenv subst + (NCicReduction.unwind t1) (NCicReduction.unwind t2) + with | Some x -> x | None -> try - unif_machines metasenv subst - (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + unif_machines metasenv subst (t1m, t2m) with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn -- 2.39.2