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 | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/formula.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/unify.ml | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 96b991e1f..87bac2fe3 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -76,11 +76,13 @@ type kind_of_formula= | Forall of constr*constr | Atom of constr +let pop t = Vars.lift (-1) t + let kind_of_formula gl term = let normalize=special_nf gl in let cciterm=special_whd gl term in match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with - Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop b)) + Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b))) |_-> match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b) 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; |