Do not ask for a normalized goal to get hypotheses and conclusions.

This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.

3 files changed, 10 insertions, 10 deletions

diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 65ba0aad04..c46817f505 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -121,11 +121,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
@@ -146,7 +146,7 @@ val is_matching_sigma : evar_map -> constr -> bool
 val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
+val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : evar_map -> constr -> bool
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e9f6231002..4bb745875b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -229,7 +229,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : ('a, 'r) Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4bf848a9c3..de35721555 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -208,7 +208,7 @@ let convert_concl ?(check=true) ty k =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-    let conclty = Proofview.Goal.raw_concl gl in
+    let conclty = Proofview.Goal.concl gl in
     Refine.refine ~unsafe:true { run = begin fun sigma ->
       let Sigma ((), sigma, p) =
         if check then begin
@@ -228,7 +228,7 @@ let convert_hyp ?(check=true) d =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-    let ty = Proofview.Goal.raw_concl gl in
+    let ty = Proofview.Goal.concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
@@ -328,7 +328,7 @@ let move_hyp id dest =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-    let ty = Proofview.Goal.raw_concl gl in
+    let ty = Proofview.Goal.concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
     let sign' = move_hyp_in_named_context sigma id dest sign in
@@ -756,7 +756,7 @@ let e_reduct_option ?(check=false) redfun = function
 let e_change_in_concl (redfun,sty) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
+    let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
     Sigma (convert_concl_no_check c sty, sigma, p)
   end }
 
@@ -4340,7 +4340,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
-  let ccl = Proofview.Goal.raw_concl gl in
+  let ccl = Proofview.Goal.concl gl in
   let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
   let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in
@@ -4409,7 +4409,7 @@ let induction_gen clear_flag isrec with_evars elim
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let evd = Sigma.to_evar_map sigma in
-  let ccl = Proofview.Goal.raw_concl gl in
+  let ccl = Proofview.Goal.concl gl in
   let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =