Merge branch 'v8.5'

5 files changed, 21 insertions, 2 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index e909a14c9e..92d4960a7c 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -42,6 +42,10 @@ TACTIC EXTEND vm_cast_no_check
   [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ]
 END
 
+TACTIC EXTEND native_cast_no_check
+  [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ]
+END
+
 TACTIC EXTEND casetype
   [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
 END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8a4b206010..547c9c5101 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -874,6 +874,15 @@ TACTIC EXTEND shelve_unifiable
     [ Proofview.shelve_unifiable ]
 END
 
+(* Unshelves the goal shelved by the tactic. *)
+TACTIC EXTEND unshelve
+| [ "unshelve" tactic0(t) ] ->
+    [
+      Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
+      Proofview.Unsafe.tclNEWGOALS gls
+    ]
+END
+
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
 [ "Unshelve" ]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bfe3097e2e..966408939d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -858,7 +858,7 @@ and interp_intro_pattern_action ist env sigma = function
   | IntroApplyOn (c,ipat) ->
       let c = { delayed = fun env sigma ->
         let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = interp_constr ist env sigma c in
+        let (sigma, c) = interp_open_constr ist env sigma c in
         Sigma.Unsafe.of_pair (c, sigma)
       } in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59a7168e51..2e7adc513a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -287,7 +287,8 @@ let apply_clear_request clear_flag dft c =
       error "keep/clear modifiers apply only to hypothesis names." in
   let clear = match clear_flag with
     | None -> dft && isVar c
-    | Some clear -> check_isvar c; clear in
+    | Some true -> check_isvar c; true
+    | Some false -> false in
   if clear then Proofview.V82.tactic (thin [destVar c])
   else Tacticals.New.tclIDTAC
 
@@ -1757,6 +1758,10 @@ let vm_cast_no_check c gl =
   let concl = Tacmach.pf_concl gl in
   Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
 
+let native_cast_no_check c gl =
+  let concl = Tacmach.pf_concl gl in
+  Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl
+
 
 let exact_proof c gl =
   let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f06a50f79c..f5695ff06e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -118,6 +118,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic
 val assumption       : unit Proofview.tactic
 val exact_no_check   : constr -> tactic
 val vm_cast_no_check : constr -> tactic
+val native_cast_no_check : constr -> tactic
 val exact_check      : constr -> unit Proofview.tactic
 val exact_proof      : Constrexpr.constr_expr -> tactic