From 8b5128c023b7217058d2f3854fc1d4ab22dd8b4b Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 2 Mar 2006 12:02:14 +0000
Subject: Correction du bug 808: il est maintenant interdit de déclarer une
 assomption en cours de preuve.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/TestRefine.v |  3 +--
 toplevel/command.ml             | 10 +++++++---
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 8ed0f7ba61..82c5cf2e74 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -97,11 +97,10 @@ Abort.
 
 
 (************************************************************************)
+Parameter f : nat * nat -> nat -> nat. 
 
 Lemma essai : nat.
 
-Parameter f : nat * nat -> nat -> nat. 
-
  refine (f _ ((fun x : nat => _:nat) 0)).
 
 Restart.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a811653cdd..72139404b5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -183,9 +183,13 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
   if is_coe then Class.try_add_new_coercion r local
 
 let declare_assumption idl is_coe k bl c =
-  let c = generalize_constr_expr c bl in
-  let c = interp_type Evd.empty (Global.env()) c in
-  List.iter (declare_one_assumption is_coe k c) idl
+  if not (Pfedit.refining ()) then 
+    let c = generalize_constr_expr c bl in
+    let c = interp_type Evd.empty (Global.env()) c in
+      List.iter (declare_one_assumption is_coe k c) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
 
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
-- 
cgit v1.2.3