diff options
| -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 *) |