forked from mattam82/Coq-Equations
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsigma_types.mli
81 lines (71 loc) · 3.02 KB
/
sigma_types.mli
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
(**********************************************************************)
(* Equations *)
(* Copyright (c) 2009-2016 Matthieu Sozeau <matthieu.sozeau@inria.fr> *)
(**********************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(**********************************************************************)
open EConstr
val mkAppG :
Evd.evar_map ref ->
Globnames.global_reference -> constr array -> constr
val applistG :
Evd.evar_map ref ->
Globnames.global_reference -> constr list -> constr
val mkSig :
Evd.evar_map ref -> Names.Name.t * types * constr -> constr
val constrs_of_coq_sigma :
Environ.env ->
Evd.evar_map ref ->
constr ->
constr -> (Names.Name.t * constr * constr * constr) list
val decompose_coq_sigma : Evd.evar_map -> constr -> (EInstance.t * constr * constr) option
val decompose_indapp : Evd.evar_map ->
constr -> constr array -> constr * constr array
val telescope :
Evd.evar_map ref ->
rel_context ->
constr * rel_context * constr
val sigmaize :
?liftty:int ->
Environ.env ->
Evd.evar_map ref ->
rel_context ->
constr ->
constr * constr * rel_context * constr list * Names.projection *
Names.projection * constr * constr
val ind_name : Names.inductive -> Names.Id.t
val declare_sig_of_ind : Environ.env -> Evd.evar_map -> bool -> Names.inductive * EConstr.EInstance.t -> constr
val get_signature :
Environ.env -> Evd.evar_map -> constr -> Evd.evar_map * constr * constr
val pattern_sigma : assoc_right:bool ->
constr ->
Names.Id.t -> Environ.env -> Evd.evar_map -> unit Proofview.tactic
(* Unused for now *)
val curry_left_hyp : Environ.env -> Evd.evar_map ->
constr -> types -> (constr * types) option
val build_sig_of_ind : Environ.env ->
Evd.evar_map ->
Names.inductive Equations_common.peuniverses ->
Evd.evar_map * constr * rel_context * constr *
constr * rel_context * int * constr
(** Pack all hypotheses into a new one using sigmas *)
val uncurry_hyps : Names.Id.t -> unit Proofview.tactic
(** Curry a term starting with a quantification on a sigma type,
associated to the right. *)
val curry : Evd.evar_map -> Names.Name.t -> constr ->
rel_context * constr
val uncurry_call : Environ.env -> Evd.evar_map -> constr ->
Evd.evar_map * constr * types
val smart_case : Environ.env -> Evd.evar_map ref -> rel_context ->
int -> types ->
rel_context * types *
(types * int * Covering.context_map) array *
int * Covering.context_map * constr list * bool
module Tactics : sig
val curry_hyp : Names.Id.t -> unit Proofview.tactic
val curry : unit Proofview.tactic
val uncurry_call : constr -> Names.Id.t -> unit Proofview.tactic
val pattern_sigma : Names.Id.t -> unit Proofview.tactic
val get_signature_pack : Names.Id.t -> Names.Id.t -> unit Proofview.tactic
end