Merge PR #6494: Remove legacy Value.normalize function.

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