diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-25 17:09:42 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-22 15:35:36 +0100 |
commit | 9bf41e6e793963ffed5171d3338bda4f91a46cd5 (patch) | |
tree | 294a4afd337a1b192ceb4a29ca49f623588487eb /plugins | |
parent | 2a056809bcd025ab59791e4f839c91c8361b77c4 (diff) |
Remove legacy Value.normalize function.
It was the identity.
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/ltac/taccoerce.ml | 18 | ||||
-rw-r--r-- | plugins/ltac/taccoerce.mli | 3 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 13 |
3 files changed, 0 insertions, 34 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9ae112d37..e5933de2a 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -61,12 +61,9 @@ struct type t = Val.t -let normalize v = v - let of_constr c = in_gen (topwit wit_constr) c let to_constr v = - let v = normalize v in if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in Some c @@ -78,7 +75,6 @@ let to_constr v = let of_uconstr c = in_gen (topwit wit_uconstr) c let to_uconstr v = - let v = normalize v in if has_type v (topwit wit_uconstr) then Some (out_gen (topwit wit_uconstr) v) else None @@ -86,7 +82,6 @@ let to_uconstr v = let of_int i = in_gen (topwit wit_int) i let to_int v = - let v = normalize v in if has_type v (topwit wit_int) then Some (out_gen (topwit wit_int) v) else None @@ -108,14 +103,12 @@ let constr_of_id env id = (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = - let v = Value.normalize v in if has_type v (topwit wit_constr_context) then out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -140,7 +133,6 @@ let g = sigma in let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -179,7 +171,6 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_var) then @@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) -> Id.to_string id @@ -206,13 +196,11 @@ let coerce_to_hint_base v = else raise (CannotCoerceTo "a hint base name") let coerce_to_int v = - let v = Value.normalize v in if has_type v (topwit wit_int) then out_gen (topwit wit_int) v else raise (CannotCoerceTo "an integer") let coerce_to_constr env v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -230,7 +218,6 @@ let coerce_to_constr env v = else fail () let coerce_to_uconstr env v = - let v = Value.normalize v in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -243,7 +230,6 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id @@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v = (* Interprets a qualified name *) let coerce_to_reference env sigma v = - let v = Value.normalize v in match Value.to_constr v with | Some c -> begin @@ -318,7 +302,6 @@ let coerce_to_reference env sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d7b253a68..dce16b733 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -31,9 +31,6 @@ module Value : sig type t = Val.t - val normalize : t -> t - (** Eliminated the leading dynamic type casts. *) - val of_constr : constr -> t val to_constr : t -> constr option val of_uconstr : Ltac_pretype.closed_glob_constr -> t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ccded4417..f2720954d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v (** More naming applications *) let name_vfun appl vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) @@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = - let v = Value.normalize v in let pr_with_env pr = match env with | Some (env,sigma) -> pr env sigma @@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with | Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -298,7 +295,6 @@ let propagate_trace ist loc id v = else Proofview.tclUNIT v let append_trace trace v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) @@ -307,11 +303,9 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = - let v = Value.normalize v in let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu @@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c = (** TODO: should use dedicated printers *) let message_of_value v = - let v = Value.normalize v in let pr_with_env pr = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in @@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg = try (** FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -1248,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with @@ -1324,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in - let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1377,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> @@ -1604,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in Proofview.tclLIFT begin |