From 486a7887579a9648c4e33a9b2c2656e7e86e780a Mon Sep 17 00:00:00 2001 From: augustin64 Date: Tue, 30 Apr 2024 11:58:29 +0200 Subject: [PATCH] Parse exact term / proof --- main.ml | 6 ++++-- parser.mly | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/main.ml b/main.ml index 1910132..f875cfd 100644 --- a/main.ml +++ b/main.ml @@ -58,8 +58,10 @@ let rec interactive ((g, gs) : proof) : proof = Goal ty -> fresh_proof ty |> interactive | Tact t -> begin match t with - Exact e -> - tact_exact (g, gs) e |> interactive + Exact_term e -> + tact_exact_term (g, gs) e |> interactive + | Exact_proof s -> + tact_exact_proof (g, gs) s |> interactive | Assumption -> tact_assumption (g, gs) |> interactive | Intro -> diff --git a/parser.mly b/parser.mly index 59d1440..c44037d 100644 --- a/parser.mly +++ b/parser.mly @@ -33,7 +33,8 @@ tactic: command: | GOAL t=ty { Goal t } - | EXACT e=expression { Tact (Exact e) } + | EXACT e=expression { Tact (Exact_term e) } + | EXACT s=TYID { Tact (Exact_proof s) } | ASSUMPTION { Tact (Assumption) } | INTRO { Tact (Intro) } | CUT t=ty { Tact (Cut t) }