From f2a4ad8b7ca2407d3dd2b6f38b70f635bd6ad0ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 25 Jun 2014 23:23:39 +0200
Subject: Putting implicit arguments of Clenv.res_pf right.

---
 proofs/clenvtac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenvtac.ml')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index b2fea6fd1..589cb5bda 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -82,7 +82,7 @@ open Unification
 
 let dft = default_unify_flags
 
-let res_pf clenv ?(with_evars=false) ?(flags=dft ()) =
+let res_pf ?(with_evars=false) ?(flags=dft ()) clenv =
   Proofview.Goal.raw_enter begin fun gl ->
     let clenv gl = clenv_unique_resolver ~flags clenv gl in
     clenv_refine with_evars (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
-- 
cgit v1.2.3