diff options
Diffstat (limited to 'plugins/firstorder/unify.ml')
| -rw-r--r-- | plugins/firstorder/unify.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d9ab36ad6..01c019744 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -21,7 +21,10 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) +let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) + let unif t1 t2= + let evd = Evd.empty in (** FIXME *) let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -47,18 +50,18 @@ let unif t1 t2= else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; |