Merge branch 'v8.5'

5 files changed, 27 insertions, 37 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 2aafaf080e..c3fe6b6574 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,8 +71,11 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let id = Namegen.id_of_name_using_hdchar env typ name in
-    let id = Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) in
+    let id = match name with
+    | Names.Anonymous -> 
+      let id = Namegen.id_of_name_using_hdchar env typ name in
+      Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
+    | Names.Name id -> id in
     let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1ffc0519fe..891e2dba51 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -25,13 +25,9 @@ open Misctypes
 DECLARE PLUGIN "extratactics"
 
 (**********************************************************************)
-(* admit, replace, discriminate, injection, simplify_eq               *)
+(* replace, discriminate, injection, simplify_eq                      *)
 (* cutrewrite, dependent rewrite                                      *)
 
-TACTIC EXTEND admit
-  [ "admit" ] -> [ admit_as_an_axiom ]
-END
-
 let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
   Tacticals.New.tclWITHHOLES false
     (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1429211f19..f894eb8fc4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -318,18 +318,16 @@ let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
   with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
-let interp_ident_gen fresh ist env sigma id =
-  try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some (env,sigma)) (dloc,id)
+let interp_ident ist env sigma id =
+  try try_interp_ltac_var (coerce_to_ident false env) ist (Some (env,sigma)) (dloc,id)
   with Not_found -> id
 
-let interp_ident = interp_ident_gen false
-let interp_fresh_ident = interp_ident_gen true
-let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) (project gl)
+let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl)
 
-(* Interprets an optional identifier which must be fresh *)
-let interp_fresh_name ist env sigma = function
+(* Interprets an optional identifier, bound or fresh *)
+let interp_name ist env sigma = function
   | Anonymous -> Anonymous
-  | Name id -> Name (interp_fresh_ident ist env sigma id)
+  | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
   try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id)
@@ -692,7 +690,7 @@ let interp_constr_with_occurrences_and_name_as_list =
     (fun ist env sigma (occ_c,na) ->
       let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
       sigma, (c_interp,
-       interp_fresh_name ist env sigma na))
+       interp_name ist env sigma na))
 
 let interp_red_expr ist env sigma = function
   | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l)
@@ -842,7 +840,7 @@ let rec interp_intro_pattern ist env sigma = function
   | loc, IntroForthcoming _  as x -> sigma, x
 
 and interp_intro_pattern_naming loc ist env sigma = function
-  | IntroFresh id -> IntroFresh (interp_fresh_ident ist env sigma id)
+  | IntroFresh id -> IntroFresh (interp_ident ist env sigma id)
   | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env sigma id
   | IntroAnonymous as x -> x
 
@@ -1213,7 +1211,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           | IntOrVarArgType ->
               Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))
           | IdentArgType ->
-              Ftactic.return (value_of_ident (interp_fresh_ident ist env sigma
+              Ftactic.return (value_of_ident (interp_ident ist env sigma
                                                (out_gen (glbwit wit_ident) x)))
           | VarArgType ->
               Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x))
@@ -1254,7 +1252,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType IdentArgType ->
               let wit = glbwit (wit_list wit_ident) in
-              let mk_ident x = value_of_ident (interp_fresh_ident ist env sigma x) in
+              let mk_ident x = value_of_ident (interp_ident ist env sigma x) in
               let ans = List.map mk_ident (out_gen wit x) in
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType t  ->
@@ -1622,7 +1620,7 @@ and interp_genarg ist env sigma concl gl x =
         (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
     | IdentArgType ->
       in_gen (topwit wit_ident)
-        (interp_fresh_ident ist env sigma (out_gen (glbwit wit_ident) x))
+        (interp_ident ist env sigma (out_gen (glbwit wit_ident) x))
     | VarArgType ->
       in_gen (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x))
     | GenArgType ->
@@ -1795,7 +1793,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let mloc = interp_move_location ist env sigma hto in
-        let ido = Option.map (interp_fresh_ident ist env sigma) ido in
+        let ido = Option.map (interp_ident ist env sigma) ido in
         name_atomic ~env
           (TacIntroMove(ido,mloc))
           (Tactics.intro_move ido mloc)
@@ -1856,7 +1854,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in
+        let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacFix(idopt,n))
           (Proofview.V82.tactic (Tactics.fix idopt n))
@@ -1868,13 +1866,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,n,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
-	  sigma , (interp_fresh_ident ist env sigma id,n,c_interp) in
+	  sigma , (interp_ident ist env sigma id,n,c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (Tactics.mutual_fix (interp_fresh_ident ist env sigma id) n l_interp 0)
+	  (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0)
           gl
       end
       end
@@ -1882,7 +1880,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in
+        let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacCofix (idopt))
           (Proofview.V82.tactic (Tactics.cofix idopt))
@@ -1894,13 +1892,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
-	  sigma , (interp_fresh_ident ist env sigma id,c_interp) in
+	  sigma , (interp_ident ist env sigma id,c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (Tactics.mutual_cofix (interp_fresh_ident ist env sigma id) l_interp 0)
+	  (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0)
           gl
       end
       end
@@ -1951,7 +1949,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
-          let na = interp_fresh_name ist env sigma na in
+          let na = interp_name ist env sigma na in
           Tacticals.New.tclWITHHOLES false
           (name_atomic ~env
             (TacLetTac(na,c_interp,clp,b,eqpat))
@@ -1967,7 +1965,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           name_atomic ~env
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
-               (let_pat_tac b (interp_fresh_name ist env sigma na)
+               (let_pat_tac b (interp_name ist env sigma na)
                   ((sigma,sigma'),c) clp eqpat) sigma')
       end
 
@@ -2077,7 +2075,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let l =
           List.map (fun (id1,id2) ->
 	    interp_hyp ist env sigma id1,
-	    interp_fresh_ident ist env sigma (snd id2)) l
+	    interp_ident ist env sigma (snd id2)) l
         in
         name_atomic ~env
           (TacRename l)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad6684e25b..b1559da33f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4411,11 +4411,6 @@ let tclABSTRACT name_op tac =
   in
   abstract_subproof s gk tac
 
-let admit_as_an_axiom =
-  Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
-  simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
-  Proofview.mark_as_unsafe
-
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.nf_enter begin fun gl ->
   try
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6025883fe6..eea4956214 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -393,8 +393,6 @@ val unify           : ?state:Names.transparent_state -> constr -> constr -> unit
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-val admit_as_an_axiom : unit Proofview.tactic
-
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> tactic