blob: 8a61590a1dbd221db4b996aa31af6c36f2acc551 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Loc
open Names
open Tac2expr
(** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
sometimes allow anti-quotations. Used for notation scopes. *)
type 'a or_anti =
| QExpr of 'a
| QAnti of Id.t located
type bindings =
| QImplicitBindings of Constrexpr.constr_expr list
| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * Constrexpr.constr_expr) Loc.located list
| QNoBindings
type intro_pattern =
| QIntroForthcoming of bool
| QIntroNaming of intro_pattern_naming
| QIntroAction of intro_pattern_action
and intro_pattern_naming =
| QIntroIdentifier of Id.t or_anti
| QIntroFresh of Id.t or_anti
| QIntroAnonymous
and intro_pattern_action =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
| QIntroInjection of intro_pattern list
(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
| QIntroRewrite of bool
and or_and_intro_pattern =
| QIntroOrPattern of intro_pattern list list
| QIntroAndPattern of intro_pattern list
type occurrences =
| QAllOccurrences
| QAllOccurrencesBut of int or_anti list
| QNoOccurrences
| QOnlyOccurrences of int or_anti list
type hyp_location = (occurrences * Id.t or_anti) * Locus.hyp_location_flag
type clause =
{ q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
type destruction_arg =
| QElimOnConstr of Constrexpr.constr_expr * bindings
| QElimOnIdent of Id.t
| QElimOnAnonHyp of int
type induction_clause = {
indcl_arg : destruction_arg;
indcl_eqn : intro_pattern_naming option;
indcl_as : or_and_intro_pattern option;
indcl_in : clause option;
}
|
