From c071747fa601c027b2e6c83903c26a8df584dd21 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Tue, 23 Jun 2015 13:27:13 +0200 Subject: [PATCH] fixing the bug about parsing non-zero level constrs --- src/reify.ml4 | 2 +- test-suite/bug6.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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