Commit 5f195649 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix compatibility wrt Coq 8.7.2 and Coq 8.9.1.

parent 6cefed83
......@@ -353,8 +353,10 @@ Fixpoint build_pt_dot_from_pt {symb word}
let X :=
match ptz in pt_zipper symb word
return match symb with T term => True | NT _ => False end ->
{ symbsq & { wordq & (parse_tree_list symbsq wordq *
ptl_zipper (symb :: symbsq) (wordq ++ word))%type } }
{ symbsq : list symbol &
{ wordq : list token &
(parse_tree_list symbsq wordq *
ptl_zipper (symb :: symbsq) (wordq ++ word))%type } }
with
| Top_ptz => fun F => False_rect _ F
| Cons_ptl_ptz ptl ptlz => fun _ =>
......
......@@ -229,7 +229,7 @@ Proof.
revert Val. generalize true at 1.
induction Hfind as [[? ?] l [?%compare_eq ?]|??? IH]=>?.
+ simpl in *; subst.
match goal with |- _ -> ?X = true => destruct X end=>//.
match goal with |- _ -> ?X = true => destruct X end; [done|].
rewrite Bool.andb_false_r. clear. induction l as [|[[[??]?]?] l IH]=>//.
+ apply IH.
- destruct future_of_prod eqn:EQ. by eapply Hval1; eauto.
......
......@@ -128,7 +128,7 @@ module Run (T: sig end) = struct
iteri (fun k constr -> fprintf f "\n | %s => %d%%positive" constr k);
fprintf f "\n end;\n";
fprintf f " surj := (fun n => match n return _ with";
iteri (fprintf f "\n | %d%%positive => %s ");
iteri (fprintf f "\n | %d%%positive => %s");
fprintf f "\n | _ => %s\n end)%%Z;\n" (List.hd constrs);
fprintf f " inj_bound := %d%%positive }.\n" (List.length constrs);
end
......@@ -512,7 +512,7 @@ module Run (T: sig end) = struct
Front.grammar.BasicSyntax.preludes;
fprintf f "From Coq.Lists Require List.\n";
fprintf f "From Coq.Numbers Require Import BinNums.\n";
fprintf f "From Coq.PArith Require Import BinPos.\n";
from_menhirlib f; fprintf f "Require Main.\n";
if not Settings.coq_no_version_check then
begin from_menhirlib f; fprintf f "Require Version.\n" end;
......
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