From f986fba6cfdbf923884da5fba4443964b0e725d5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 30 Mar 2010 14:33:54 +0000
Subject: Manual qualification of Mfourier.Proof in micromega to avoid ocamldep
 using ide/proof

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/certificate.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index c5760229c5..7ddcf35d3a 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -486,7 +486,7 @@ let raw_certificate l =
       match Fourier.find_point p with
 	| Inr prf ->
 	    if debug then Printf.printf "AProof : %a\n" pp_proof prf ;
-	    let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in
+	    let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Mfourier.Proof.mk_proof p prf))) in
 	      if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ;
 	      Some (rats_to_ints (Vect.to_list cert))
 	| Inl _   -> None
-- 
cgit v1.2.3