diff src/Reflection.v @ 547:2c8c693ddaba

Fixes for Coq 8.6
author Adam Chlipala <adam@chlipala.net>
date Wed, 12 Jul 2017 13:08:24 -0400
parents ed829eaa91b2
children
line wrap: on
line diff
--- a/src/Reflection.v	Thu May 12 18:09:36 2016 -0500
+++ b/src/Reflection.v	Wed Jul 12 13:08:24 2017 -0400
@@ -673,7 +673,7 @@
   let b := inList x xs in
     match b with
       | true => xs
-      | false => constr:(x, xs)
+      | false => constr:((x, xs))
     end.
 
 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *)
@@ -718,8 +718,8 @@
 
 Ltac reifyTerm xs e :=
   match e with
-    | True => constr:Truth'
-    | False => constr:Falsehood'
+    | True => Truth'
+    | False => Falsehood'
     | ?e1 /\ ?e2 =>
       let p1 := reifyTerm xs e1 in
       let p2 := reifyTerm xs e2 in