diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 15:50:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (patch) | |
| tree | 4ab6481d8d182f6bb3dd241b7112a3027aa26b2a /plugins/firstorder/unify.ml | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'plugins/firstorder/unify.ml')
| -rw-r--r-- | plugins/firstorder/unify.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 5520c7e35..7cbfb8e7d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -24,6 +24,8 @@ exception UFAIL of constr*constr let strip_outer_cast t = EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) +let pop t = Vars.lift (-1) t + let unif t1 t2= let evd = Evd.empty in (** FIXME *) let bige=Queue.create () @@ -62,7 +64,7 @@ let unif t1 t2= | 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 (EConstr.of_constr b),pop (EConstr.of_constr d)) bige + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; |