fixing the bug about parsing non-zero level constrs

gmalecha · Jun 23, 2015 · c071747 · c071747
1 parent 95bf7e5
commit c071747
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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! **)
+Quote Definition qTwo := 1 + 1.