From a684010f1a926c6fa1649b1a6c386645bd520a21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Mar 2015 14:28:28 +0100 Subject: Reverting r10021 which enforces early assumptions on freshness which seem to be overly strong in practice (see discussion related to #4035). --- tactics/tacinterp.ml | 44 +++++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 23 deletions(-) (limited to 'tactics/tacinterp.ml') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1429211f1..f894eb8fc 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) -- cgit v1.2.3