diff options
| author | coq | 2006-03-02 12:02:14 +0000 |
|---|---|---|
| committer | coq | 2006-03-02 12:02:14 +0000 |
| commit | 8b5128c023b7217058d2f3854fc1d4ab22dd8b4b (patch) | |
| tree | 34dd224c14814234d9fecfb16dce84b740f4ef44 | |
| parent | 2292dd89b9b36ec8c865ab67e5291088bfcc4806 (diff) | |
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
| -rw-r--r-- | test-suite/success/TestRefine.v | 3 | ||||
| -rw-r--r-- | 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 *) |