aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml61
-rw-r--r--proofs/clenv.mli4
-rw-r--r--proofs/clenvtac.ml4
-rw-r--r--proofs/clenvtac.mli4
-rw-r--r--proofs/evar_refiner.ml6
-rw-r--r--proofs/evar_refiner.mli4
-rw-r--r--proofs/goal.ml6
-rw-r--r--proofs/goal.mli4
-rw-r--r--proofs/goal_select.ml4
-rw-r--r--proofs/goal_select.mli4
-rw-r--r--proofs/logic.ml4
-rw-r--r--proofs/logic.mli5
-rw-r--r--proofs/miscprint.ml4
-rw-r--r--proofs/miscprint.mli4
-rw-r--r--proofs/proof.ml4
-rw-r--r--proofs/proof.mli4
-rw-r--r--proofs/proof_bullet.ml4
-rw-r--r--proofs/proof_bullet.mli4
-rw-r--r--proofs/refine.ml4
-rw-r--r--proofs/refine.mli4
-rw-r--r--proofs/refiner.ml14
-rw-r--r--proofs/refiner.mli4
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli16
-rw-r--r--proofs/tactypes.ml4
25 files changed, 125 insertions, 59 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b0eb8dc646..37d54a4eea 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -249,6 +249,63 @@ let clenv_dependent ce = clenv_dependent_gen false ce
(******************************************************************)
+(* Instantiate metas that create beta/iota redexes *)
+
+let meta_reducible_instance evd b =
+ let fm = b.freemetas in
+ let fold mv accu =
+ let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
+ match fvalue with
+ | None -> accu
+ | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
+ in
+ let metas = Metaset.fold fold fm Metamap.empty in
+ let rec irec u =
+ let u = whd_betaiota Evd.empty u (* FIXME *) in
+ match EConstr.kind evd u with
+ | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
+ let m = destMeta evd (strip_outer_cast evd c) in
+ (match
+ try
+ let g, s = Metamap.find m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if isConstruct evd g || not is_coerce then Some g else None
+ with Not_found -> None
+ with
+ | Some g -> irec (mkCase (ci,p,g,bl))
+ | None -> mkCase (ci,irec p,c,Array.map irec bl))
+ | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
+ let m = destMeta evd (strip_outer_cast evd f) in
+ (match
+ try
+ let g, s = Metamap.find m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if isLambda evd g || not is_coerce then Some g else None
+ with Not_found -> None
+ with
+ | Some g -> irec (mkApp (g,l))
+ | None -> mkApp (f,Array.map irec l))
+ | Meta m ->
+ (try let g, s = Metamap.find m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if not is_coerce then irec g else u
+ with Not_found -> u)
+ | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
+ let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
+ (match
+ try
+ let g, s = Metamap.find m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if isConstruct evd g || not is_coerce then Some g else None
+ with Not_found -> None
+ with
+ | Some g -> irec (mkProj (p,g))
+ | None -> mkProj (p,c))
+ | _ -> EConstr.map evd irec u
+ in
+ if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
+ else irec b.rebus
+
let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
{ clenv with
evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7213c9318c..1adfdb885a 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c6a0299cf3..767f93787d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 2357a1fe30..6eafca359b 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8297b11585..53254e9511 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) env sigma =
let env = Evd.evar_filtered_env env evi in
let sigma',typed_c =
let flags = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a618bf1c94..61e22e5874 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4759c0860f..b1f8fd3e97 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -131,4 +131,4 @@ module V82 = struct
end
-module Set = Set.Make(struct type t = goal let compare = Evar.compare end)
+module Set = Evar.Set
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 7b16d869e9..a3aa1e248f 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index 36b50d9e9f..29e19778e4 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
index c322ace9f3..977392baa6 100644
--- a/proofs/goal_select.mli
+++ b/proofs/goal_select.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index bac13fcfc3..406e71aafc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 1046fd8b29..ef8b2731b2 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -50,6 +50,7 @@ exception RefinerError of Environ.env * evar_map * refiner_error
val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
val catchable_exception : exn -> bool
+[@@ocaml.deprecated "This function does not scale in the presence of dynamically added exceptions. Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
(** Move destination for hypothesis *)
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 1092e290c7..af30d3d727 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 70a3726605..cbb9c45d7e 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 7d0b31734e..21006349d2 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 134b0146b6..1a0b105723 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index d978885d62..f1f7361317 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ef4530a363..687781361c 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index ea42218aaa..0bf0cd7b63 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 269382489d..d11616db3f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fd73ab1b5a..75c3436cf4 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -204,14 +204,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
let catch_failerror (e, info) =
- if catchable_exception e then Control.check_for_interrupt ()
- else match e with
- | FailError (0,_) ->
- Control.check_for_interrupt ()
- | FailError (lvl,s) ->
+ match e with
+ | FailError (lvl,s) when lvl > 0 ->
Exninfo.iraise (FailError (lvl - 1, s), info)
- | e -> Exninfo.iraise (e, info)
- (** FIXME: do we need to add a [Errors.push] here? *)
+ | e -> Control.check_for_interrupt ()
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
let tclORELSE0 t1 t2 g =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 7f8e24fc0e..66eae1db81 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 3e4549f92c..0bac0b0424 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index b4247f39b9..d8f7b7eed8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -37,6 +37,7 @@ val pf_unsafe_type_of : Goal.goal sigma -> constr -> types
[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."]
val pf_type_of : Goal.goal sigma -> constr -> evar_map * types
val pf_hnf_type_of : Goal.goal sigma -> constr -> types
+[@@ocaml.deprecated "This is a no-op now"]
val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration
val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types
@@ -49,22 +50,33 @@ val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
val pf_reduce :
(env -> evar_map -> constr -> constr) ->
Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
+
val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
Goal.goal sigma -> constr -> evar_map * constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_whd_all : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_hnf_constr : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_nf : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_nf_betaiota : Goal.goal sigma -> constr -> constr
val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+[@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"]
val pf_compute : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use Tacred.unfoldn"]
val pf_const_value : Goal.goal sigma -> pconstant -> constr
+[@@ocaml.deprecated "Use Environ.constant_value_in"]
val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : Goal.goal sigma -> Pp.t
diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml
index 634faf1acc..cbe62d1945 100644
--- a/proofs/tactypes.ml
+++ b/proofs/tactypes.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 02:39:05 +0000