diff --git a/src/reify.ml4 b/src/reify.ml4 index 566c8f057..922d6bed9 100644 --- a/src/reify.ml4 +++ b/src/reify.ml4 @@ -621,7 +621,7 @@ TACTIC EXTEND get_goal END;; VERNAC COMMAND EXTEND Make_vernac CLASSIFIED AS SIDEFF - | [ "Quote" "Definition" ident(name) ":=" constr(def) ] -> + | [ "Quote" "Definition" ident(name) ":=" lconstr(def) ] -> [ check_inside_section () ; let (evm,env) = Lemmas.get_current_context () in let def = Constrintern.interp_constr env evm def in diff --git a/test-suite/bug6.v b/test-suite/bug6.v index 6e6e36091..51d8ddf17 100644 --- a/test-suite/bug6.v +++ b/test-suite/bug6.v @@ -2,4 +2,4 @@ Require Import Template.Template. Quote Definition qOne := 1. Quote Definition qOne_red := Eval compute in 1. -Quote Definition qTwo := 1 + 1. (** This should succeed! **) \ No newline at end of file +Quote Definition qTwo := 1 + 1. \ No newline at end of file