From 33019e47a55caf3923d08acd66077f0a52947b47 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 2 Dec 1999 09:45:07 +0000
Subject: Pfedit (fin)

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

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a9a8e0d3b6..9fc3768552 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -260,7 +260,7 @@ let start_proof_with_type na str env concl =
 let start_proof na str concl_com =
   let sigma = Evd.empty in
   let env = Global.env() in
-  let concl = fconstruct_type sigma (Environ.context env) concl_com in
+  let concl = type_of_com env concl_com in
   start_proof_with_type na str env concl.body
 
 let start_proof_constr na str concl =
-- 
cgit v1.2.3