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 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
|
(************************************************************************)
(* * 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 Names
open EConstr
open Proofview
(** Redefinition of Ltac1 data structures because of impedance mismatch *)
type evars_flag = bool
type advanced_flag = bool
type 'a thunk = (unit, 'a) Tac2ffi.fun1
type quantified_hypothesis = Tactypes.quantified_hypothesis =
| AnonHyp of int
| NamedHyp of lident
type explicit_bindings = (quantified_hypothesis * EConstr.t) list
type bindings =
| ImplicitBindings of EConstr.t list
| ExplicitBindings of explicit_bindings
| NoBindings
type constr_with_bindings = EConstr.constr * bindings
type core_destruction_arg =
| ElimOnConstr of constr_with_bindings tactic
| ElimOnIdent of Id.t
| ElimOnAnonHyp of int
type destruction_arg = core_destruction_arg
type intro_pattern =
| IntroForthcoming of bool
| IntroNaming of intro_pattern_naming
| IntroAction of intro_pattern_action
and intro_pattern_naming =
| IntroIdentifier of Id.t
| IntroFresh of Id.t
| IntroAnonymous
and intro_pattern_action =
| IntroWildcard
| IntroOrAndPattern of or_and_intro_pattern
| IntroInjection of intro_pattern list
| IntroApplyOn of EConstr.t thunk * intro_pattern
| IntroRewrite of bool
and or_and_intro_pattern =
| IntroOrPattern of intro_pattern list list
| IntroAndPattern of intro_pattern list
type occurrences =
| AllOccurrences
| AllOccurrencesBut of int list
| NoOccurrences
| OnlyOccurrences of int list
type hyp_location_flag = Locus.hyp_location_flag =
| InHyp | InHypTypeOnly | InHypValueOnly
type hyp_location = Id.t * occurrences * hyp_location_flag
type clause =
{ onhyps : hyp_location list option;
concl_occs : occurrences }
type induction_clause =
destruction_arg *
intro_pattern_naming option *
or_and_intro_pattern option *
clause option
type multi = Equality.multi =
| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus
type orientation = bool
type rewriting =
orientation option *
multi *
constr_with_bindings tactic
type assertion =
| AssertType of intro_pattern option * constr * unit thunk option
| AssertValue of Id.t * constr
|