diff --git a/CHANGES.md b/CHANGES.md
index 36acf9137..d9663ffff 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -24,6 +24,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
 - Extend `print` query to the following arguments: `verbose`, `debug`, `flag`, `builtin`, `prover`, `prover_timeout`.
 - add a version number to the header of the index db file to prevent crash of LP when the structure of db changes.
+- Tactic `#with_goal t` which calls term tactic t with current goal of type Prop as parameter.
 
 ### Changed
 
@@ -37,6 +38,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Type of `#assume` in order to generate a new symbol and use it inside a tactic term.
 - Errors occurring while a proof is in progress now report the proof state: the goals a failing tactic was applied to, the goals before and after the tactic for a subproof-count mismatch, and the remaining goals when a proof is unfinished at `end`. The state is printed after the error message, which stays unchanged. The LSP server does not attach the proof state to tactic failures since editors display it themselves.
 - Lambdapi does not use Cmdliner anymore.
+>>>>>>> dk/master
 
 ### Fixed
 
diff --git a/doc/structure.rst b/doc/structure.rst
index ec7b20853..3273b8b1f 100644
--- a/doc/structure.rst
+++ b/doc/structure.rst
@@ -87,6 +87,7 @@ Overview of directories and files
 
   * ``command.ml``: command handling
   * ``compile.ml``: file parsing and compiling (.lpo files)
+  * ``gconf.ml``: builtins needed to build current goal (tactic #with_goal)
   * ``inductive.ml``: generation of induction principles
   * ``query.ml``: handling of queries (commands that do not change the signature or the proof state)
 
diff --git a/doc/tacticals.rst b/doc/tacticals.rst
index dcb760e68..6d683ca99 100644
--- a/doc/tacticals.rst
+++ b/doc/tacticals.rst
@@ -51,6 +51,7 @@ The BNF grammar of tactics is in `lambdapi.bnf <https://raw.githubusercontent.co
    builtin "symmetry" ≔ …; // : T
    builtin "try" ≔ …; // : T → T
    builtin "why3" ≔ …; // : T
+   builtin "with_goal" ≔ …; // (Prop → T) → T
 
 The tactics taking a string as argument need the ``"String"`` :ref:`builtin` to be set. The string argument of ``refine`` is parsed as a term, and thus can contain underscores. If the builtin ``"and"`` is mapped to some symbol, say ``&``, then ``& t u`` is interpreted as follows: the tactic ``t`` is applied and, in case of success, the tactic ``u`` is applied. All other symbols are interpreted by the corresponding tactics.
 
@@ -103,3 +104,8 @@ An example of use is given in `Tactic.lp <https://github.com/Deducteam/lambdapi/
 -------
 
 ``try t`` applies ``t``. If ``t`` fails, then ``try t`` leaves the goal unchanged.
+
+``with_goal``
+-------------
+
+``with_goal t`` calls term tactic ``t`` on the current goal seen as a Prop. builtins must be defined to map Prf, El, => and forAll.
diff --git a/src/core/builtin.ml b/src/core/builtin.ml
index 4ecd45472..9a7af0057 100644
--- a/src/core/builtin.ml
+++ b/src/core/builtin.ml
@@ -240,6 +240,7 @@ let _ =
   register_typ "solve" tac;
   register_typ "symmetry" tac;
   register_typ "try" (arr tac tac);
-  register_typ "why3" tac
+  register_typ "why3" tac;
+  register_typ "with_goal" (arr (arr prop tac) tac);
 
 end
diff --git a/src/core/sign.ml b/src/core/sign.ml
index a3bd6954f..f42bb3844 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -112,7 +112,7 @@ let link : t -> unit = fun sign ->
               StrMap.add s.sym_name s !(Ghost.sign.sign_symbols);
             s
           end
-        else assert false
+        else begin failwith s.sym_name end
   in
   let link_term mk_Appl =
     let rec link_term t =
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
index 1ed80ea2c..2e34ae4da 100644
--- a/src/handle/tactic.ml
+++ b/src/handle/tactic.ml
@@ -226,6 +226,7 @@ type tactic =
   | T_symmetry
   | T_try
   | T_why3
+  | T_with_goal
 
 type config = (string,tactic) Hashtbl.t
 
@@ -263,6 +264,7 @@ let get_config (ss:Sig_state.t) (pos:Pos.popt) : config =
   add "symmetry" T_symmetry;
   add "try" T_try;
   add "why3" T_why3;
+  add "with_goal" T_with_goal;
   t
 
 (** [p_term pos t] converts the term [t] into a p_term at position [pos]. *)
@@ -298,6 +300,7 @@ let p_term (ss:Sig_state.t) (pos:popt): int StrMap.t -> term -> p_term =
         let id = Pos.make pos (base_name x) in
         P_LLet(id,[],Some(term idmap a),term idmap t,term idmap' b)
     | Meta _ -> P_Wild
+    | Plac _ -> P_Wild
     | _ -> fatal pos "Unhandled term expression: %a." Print.term t
   in term
 
@@ -379,7 +382,6 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
       then Some new_ps
       else None
     with Fatal _ -> None
-
   (* [p_tactic ss g env pos t] weak head normalizes [t] and converts the
      result into a p_tactic. *)
   and p_tactic (ps:proof_state) (g:goal) (env:Env.t) (pos:Pos.popt)
@@ -476,11 +478,12 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
             | T_try, [t] -> ps, mk(P_tac_try(tac_eval t))
             | T_try, _ -> assert false
             | T_why3, _ -> ps, mk(P_tac_why3 None)
+            | T_with_goal, [t] -> ps, mk (P_tac_with_goal(p_term t))
+            | T_with_goal, _ -> assert false
           with Not_found ->
             fatal pos "Unhandled tactic expression: %a." term t
         end
       | _ -> fatal pos "Unhandled tactic expression: %a." term t
-
   and handle ps ({elt;pos} as tac) =
   if Logger.log_enabled() then log "%a" Pretty.tactic tac;
   match ps.proof_goals with
@@ -781,6 +784,22 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
             Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
         | _ -> assert false
       end
+  | P_tac_with_goal t ->
+      let prf = Builtin.get ss pos [] "Prf" in
+      let prop = Builtin.get ss pos [] "Prop" in
+      let p = new_problem() in
+      let n = List.length env in
+      let m = LibMeta.fresh p (Env.to_prod env (mk_Symb prop)) n in
+      let goal = mk_Meta(m,Env.to_terms env) in
+      let c = (ctxt g,(mk_Appl (mk_Symb prf, goal)), gt.goal_type) in
+      p := {!p with to_solve = c::!p.to_solve};
+      if not (Unif.solve_noexn p) || !p.unsolved <> [] || !p.to_solve <> []
+      then fatal pos "Cannot unify goal with (Prf _)";
+      let t = scope t in
+      let t = mk_Appl (t, goal) in
+      if (Logger.log_enabled ()) then log "WITH_GOAL [%a]" term goal;
+      let ps,t = p_tactic ps g env pos t in
+      handle ps t
   | P_tac_try t ->
       begin try handle ps t with Fatal _ -> ps end
   | P_tac_orelse(t1,t2) ->
@@ -805,7 +824,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
           fatal pt.pos "Cannot infer the type of [%a]" term t
       | Some(t,_) ->
         if Unif.solve_noexn p then
-          let ps, t = p_tactic ps g env pos t in handle ps t
+          let ps,t = p_tactic ps g env pos t in handle ps t
         else fatal pos "Cannot solve typing constraints for [%a]" term t
 
   in handle
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index 0200341f2..e7c54d3df 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -357,6 +357,7 @@ let rec tactic : p_tactic pp = fun ppf { elt;  _ } ->
   | P_tac_why3 p ->
       let prover ppf s = out ppf " \"%s\"" s in
       out ppf "why3%a" (Option.pp prover) p
+  | P_tac_with_goal t -> out ppf "with_goal %a" term t
 
 let rec subproof : p_subproof pp = fun ppf sp ->
   out ppf "{@[<hv2>@ %a@ @]}" proofsteps sp
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index 2e1e096ec..4addbf7b8 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -305,6 +305,7 @@ type p_tactic_aux =
   | P_tac_sym
   | P_tac_try of p_tactic
   | P_tac_why3 of string option
+  | P_tac_with_goal of p_term
 
 and p_tactic = p_tactic_aux loc
 
@@ -359,6 +360,7 @@ let tactic_keyword : p_tactic -> string option = fun {elt;_} ->
   | P_tac_sym -> Some "symmetry"
   | P_tac_try _ -> Some "try"
   | P_tac_why3 _ -> Some "why3"
+  | P_tac_with_goal _ -> Some "with_goal"
 
 (** [tactic_keyword_pos t] returns the position of the keyword introducing
     tactic [t], or the position of the whole of [t] when no single keyword
@@ -554,6 +556,7 @@ let eq_p_tactic : p_tactic eq = fun {elt=t1;_} {elt=t2;_} ->
   match t1, t2 with
   | P_tac_all_hyps t1, P_tac_all_hyps t2
   | P_tac_first_hyp t1, P_tac_first_hyp t2
+  | P_tac_with_goal t1, P_tac_with_goal t2
   | P_tac_apply t1, P_tac_apply t2
   | P_tac_refine t1, P_tac_refine t2 -> eq_p_term t1 t2
   | P_tac_have(i1,t1), P_tac_have(i2,t2) ->
@@ -774,6 +777,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_tac_refl
     | P_tac_sym
     | P_tac_why3 _
+    | P_tac_with_goal _
     | P_tac_solve
     | P_tac_fail
     | P_tac_focus _
diff --git a/tests/OK/Tactic.lp b/tests/OK/Tactic.lp
index 93a52dfa7..e35e23d16 100644
--- a/tests/OK/Tactic.lp
+++ b/tests/OK/Tactic.lp
@@ -89,6 +89,9 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
+constant symbol #with_goal : (Prop → Tactic) → Tactic;
+builtin "with_goal" ≔ #with_goal;
+
 // defined tactics
 
 symbol nothing ≔ #try #fail;
diff --git a/tests/OK/with_goal.lp b/tests/OK/with_goal.lp
new file mode 100644
index 000000000..434c7480c
--- /dev/null
+++ b/tests/OK/with_goal.lp
@@ -0,0 +1,15 @@
+require open tests.OK.Prop tests.OK.Set tests.OK.FOL tests.OK.Univ;
+require open tests.OK.Tactic;
+
+constant symbol T: Set;
+constant symbol P: τ T → Prop;
+
+sequential symbol prove: Prop → Tactic;
+rule prove (@∀ $T $P) ↪ #assume "x" (λ (x: τ $T), prove ($P x))
+with prove ($P ⇒ $Q) ↪ #assume "h" (λ (h: π $P), prove $Q)
+with prove _ ↪ #print "" & #assumption;
+
+symbol test : Π x:τ T,  π (P x) → π (P x) ≔
+begin
+  eval (#with_goal (λ g:Prop, #set "g1" [prop] g & #print "" & prove g));
+end;
diff --git a/tests/export_dk.sh b/tests/export_dk.sh
index 9178bfa35..4dff89e75 100755
--- a/tests/export_dk.sh
+++ b/tests/export_dk.sh
@@ -43,9 +43,8 @@ do
         # require escaped module name
         π/utf_path|escape_path|'a b/escape file'|require_nondkmident|262_pair_ex_2|require_symbol);;
         # use builtin strings
-        Tactic);;
         # requires Tactic
-        1374|assume|first_hyp|all_hyps|1493);;
+        1374|Tactic|assume|first_hyp|all_hyps|with_goal|1493);;
         # default case
         *) translate $f.lp;;
     esac
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index d3a8b3411..582c2dd8f 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -57,7 +57,7 @@ do
         # module alias
         alias);;
         # proofs
-        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps|1435_part2|1435);;
+        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps|with_goal|1435_part2|1435);;
         # "open"
         triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|1374|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151|B1|B2|C1|C2|C3|Epsilon|1313|FunExt|Prod|Conj|Disj|ExtraRules|Univ|1493);;
         # "inductive"