1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* 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 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Locus
open Evd
open Pretype_errors
open Environ
open EConstr
(** Finding subterms, possibly up to some unification function,
possibly at some given occurrences *)
exception SubtermUnificationError of subterm_unification_error
(** A testing function is typically a unification function returning a
substitution or failing with Error, together with a function to merge
substitutions and an initial substitution;
last_found is used for error messages and it has to be initialized
with None. *)
type ('a, 'b) testing_function = {
match_fun : int -> 'a -> constr -> ('b, unit) Result.t;
merge_fun : 'b -> 'a -> ('a, unit) Result.t;
mutable testing_state : 'a;
mutable last_found : position_reporting option
}
(** This is the basic testing function, looking for exact matches of a
closed term *)
val make_eq_univs_test : env -> evar_map -> constr -> (evar_map, evar_map) testing_function
(** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
modulo a testing function [test] and replaces successfully
matching subterms at the indicated occurrences [occl] with [mk
()]; it turns an Error value returned by the [merge_fun]
function into a SubtermUnificationError. *)
val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first ->
('a, 'b) testing_function -> (unit -> constr) -> constr -> constr
(** [replace_term_occ_decl_modulo] is similar to
[replace_term_occ_modulo] but for a named_declaration. *)
val replace_term_occ_decl_modulo :
env -> evar_map ->
(occurrences * hyp_location_flag) or_like_first ->
('a, 'b) testing_function -> (unit -> constr) ->
named_declaration -> named_declaration
(** [subst_closed_term_occ occl c d] replaces occurrences of
closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
unifying universes which results in a set of constraints. *)
val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
constr -> constr -> constr * evar_map
(** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of
closed [c] at positions [occl] by [Rel 1] in [decl]. *)
val subst_closed_term_occ_decl : env -> evar_map ->
(occurrences * hyp_location_flag) or_like_first ->
constr -> named_declaration -> named_declaration * evar_map
|
