From 06cbdda6e25ccb83e3d23963df7026043c678a06 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Mon, 11 Jul 2016 18:03:20 +0200 Subject: [PATCH] Make reshape_val work on non-trivial values --- heap_lang/tactics.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v index 336f4043f..4436ec429 100644 --- a/heap_lang/tactics.v +++ b/heap_lang/tactics.v @@ -25,13 +25,13 @@ Ltac reshape_val e tac := let rec go e := match e with | of_val ?v => v - | wexpr' ?e => reshape_val e tac + | wexpr' ?e => go e | Rec ?f ?x ?e => constr:(RecV f x e) | Lit ?l => constr:(LitV l) | Pair ?e1 ?e2 => - let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2) - | InjL ?e => let v := reshape_val e in constr:(InjLV v) - | InjR ?e => let v := reshape_val e in constr:(InjRV v) + 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]. Ltac reshape_expr e tac := -- GitLab