From 2869d9059f3b6714ab6d12e76f8fb84a91db4bcd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Aug 2014 16:49:21 -0700
Subject: [PATCH] feat(frontends/lean): change 'proof-qed' semantics: no
 backtracking

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp  | 7 ++++---
 src/library/tactic/expr_to_tactic.cpp | 3 +++
 src/library/tactic/expr_to_tactic.h   | 1 +
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 1037dd718..9855f1f42 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -149,10 +149,11 @@ static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &
         auto pos = p.pos();
         expr tac = p.parse_expr();
         if (use_exact)
-            tac = p.save_pos(mk_app(get_exact_tac_fn(), tac), pos);
+            tac = p.mk_app(get_exact_tac_fn(), tac, pos);
         if (pre_tac)
-            tac = p.save_pos(mk_app(get_and_then_tac_fn(), *pre_tac, tac), pos);
-        r = r ? p.save_pos(mk_app(get_and_then_tac_fn(), *r, tac), pos) : tac;
+            tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
+        tac = p.mk_app(get_determ_tac_fn(), tac, pos);
+        r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac;
         if (p.curr_is_token(g_qed)) {
             auto pos = p.pos();
             p.next();
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index d1afa7696..b6eadc09d 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -29,12 +29,15 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
 static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_builtin_tac_name(g_tac, "builtin_tactic");
 static name g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
 static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat"), g_fixpoint_name(g_tac, "fixpoint");
+static name g_determ_tac_name(g_tac, "determ");
 static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
 static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
+static expr g_determ_tac_fn(Const(g_determ_tac_name));
 static expr g_tac_type(Const(g_tac_name)), g_builtin_tac(Const(g_builtin_tac_name)), g_fixpoint_tac(Const(g_fixpoint_name));
 expr const & get_exact_tac_fn() { return g_exact_tac_fn; }
 expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; }
 expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; }
+expr const & get_determ_tac_fn() { return g_determ_tac_fn; }
 expr const & get_repeat_tac_fn() { return g_repeat_tac_fn; }
 expr const & get_tactic_type() { return g_tac_type; }
 
diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h
index 8eb6bbc26..b6ec14267 100644
--- a/src/library/tactic/expr_to_tactic.h
+++ b/src/library/tactic/expr_to_tactic.h
@@ -45,6 +45,7 @@ expr const & get_exact_tac_fn();
 expr const & get_and_then_tac_fn();
 expr const & get_or_else_tac_fn();
 expr const & get_repeat_tac_fn();
+expr const & get_determ_tac_fn();
 
 /** \brief Exception used to report a problem when an expression is being converted into a tactic. */
 class expr_to_tactic_exception : public tactic_exception {