diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-01 18:37:50 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-04-02 10:27:49 -0400 |
commit | 83d035c40eb8f4f66097c003f90fab0a58fa25d8 (patch) | |
tree | c82b74b80e511d9afcf32b5abc8d2fb05a05b199 | |
parent | d5006369495a4e79c4db011d8fdb334b266381f2 (diff) |
Work around bug #5434
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute]
breaks an invariant asserted on line 115 of
pretyping/constr_matching.ml. This was triggering whenever we tried to
reify one of the operations.
-rw-r--r-- | src/NewBaseSystem.v | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index d962dae99..9f7a327bc 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -903,6 +903,34 @@ Positional.to_associational_cps Positional.to_associational Positional.eval Posi (@runtime_mul)); [replace_with_vm_compute t1; clear t1|reflexivity]. +(** This block of tactic code works around bug #5434 + (https://coq.inria.fr/bugs/show_bug.cgi?id=5434), that + [vm_compute] breaks an invariant in pretyping/constr_matching.ml. + So we refresh all of the names in match statements in the goal by + crawling it. *) +Ltac replace_match_with_destructuring_match T := + match T with + | ?F ?X + => let F' := replace_match_with_destructuring_match F in + let X' := replace_match_with_destructuring_match X in + constr:(F' X') + (* we must use [@?f a b] here and not [?f], or else we get an anomaly *) + | match ?d with pair a b => @?f a b end + => let d' := replace_match_with_destructuring_match d in + let T' := fresh in + constr:(let '(a, b) := d' in + match f a b with + | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in + let v := replace_match_with_destructuring_match v in + exact v) + end) + | ?x => x + end. +Ltac do_replace_match_with_destructuring_match_in_goal := + let G := get_goal in + let G' := replace_match_with_destructuring_match G in + change G'. + (* TODO : move *) Lemma F_of_Z_opp {m} x : F.of_Z m (- x) = F.opp (F.of_Z m x). Proof. @@ -926,6 +954,7 @@ Ltac solve_op_mod_eq wt x := reflexivity]; cbv [mod_eq]; apply f_equal2; [|reflexivity]; apply f_equal; - basesystem_partial_evaluation_RHS. + basesystem_partial_evaluation_RHS; + do_replace_match_with_destructuring_match_in_goal. Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x. |