Commit 21d4658d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Correct a bug in reshape_expr.

parent 4461668a
......@@ -260,7 +260,7 @@ Ltac reshape_val e tac :=
let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
| InjL ?e => let v := go e in constr:(InjLV v)
| InjR ?e => let v := go e in constr:(InjRV v)
end in let v := go e in first [tac v | fail 2].
end in let v := go e in tac v.
Ltac reshape_expr e tac :=
let rec go K e :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment