diff options
Diffstat (limited to 'AAC_coq.mli')
| -rw-r--r-- | AAC_coq.mli | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/AAC_coq.mli b/AAC_coq.mli index 116ff4c..a0f2ce0 100644 --- a/AAC_coq.mli +++ b/AAC_coq.mli @@ -10,7 +10,7 @@ and we import several definitions from Coq's standard library. This general purpose library could be reused by other plugins. - + Some salient points: - we use Caml's module system to mimic Coq's one, and avoid cluttering the namespace; @@ -27,18 +27,18 @@ val init_constant : string list -> string -> Term.constr (** {2 General purpose functions} *) -type goal_sigma = Proof_type.goal Tacmach.sigma +type goal_sigma = Proof_type.goal Tacmach.sigma val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma -val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic val nf_evar : goal_sigma -> Term.constr -> Term.constr val fresh_evar :goal_sigma -> Term.types -> Term.constr* goal_sigma val evar_unit :goal_sigma ->Term.constr -> Term.constr* goal_sigma -val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic (** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) -val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term @@ -51,7 +51,7 @@ module List: sig (** [of_list ty l] *) val of_list:Term.constr ->Term.constr list ->Term.constr - + (** [type_of_list ty] *) val type_of_list:Term.constr ->Term.constr end @@ -77,7 +77,7 @@ module Comparison : sig val gt : Term.constr lazy_t end -module Leibniz : sig +module Leibniz : sig val eq_refl : Term.types -> Term.constr -> Term.constr end @@ -85,7 +85,7 @@ module Option : sig val some : Term.constr -> Term.constr -> Term.constr val none : Term.constr -> Term.constr val of_option : Term.constr -> Term.constr option -> Term.constr -end +end (** Coq positive numbers (pos) *) module Pos: @@ -108,14 +108,14 @@ sig val mk_equivalence: Term.constr -> Term.constr -> Term.constr val mk_reflexive: Term.constr -> Term.constr -> Term.constr val mk_transitive: Term.constr -> Term.constr -> Term.constr -end +end module Relation : sig type t = {carrier : Term.constr; r : Term.constr;} - val make : Term.constr -> Term.constr -> t + val make : Term.constr -> Term.constr -> t val split : t -> Term.constr * Term.constr end - + module Transitive : sig type t = { @@ -125,7 +125,7 @@ module Transitive : sig } val make : Term.constr -> Term.constr -> Term.constr -> t val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic val to_relation : t -> Relation.t end @@ -135,11 +135,11 @@ module Equivalence : sig { carrier : Term.constr; eq : Term.constr; - equivalence : Term.constr; - } + equivalence : Term.constr; + } val make : Term.constr -> Term.constr -> Term.constr -> t val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic val to_relation : t -> Relation.t val split : t -> Term.constr * Term.constr * Term.constr @@ -171,7 +171,7 @@ val warning : string -> unit (** {2 Rewriting tactics used in aac_rewrite} *) -module Rewrite : sig +module Rewrite : sig (** The rewriting tactics used in aac_rewrite, build as handlers of the usual [setoid_rewrite]*) @@ -179,11 +179,11 @@ module Rewrite : sig (** {2 Datatypes} *) (** We keep some informations about the hypothesis, with an (informal) - invariant: + invariant: - [typeof hyp = typ] - [typ = forall context, body] - [body = rel left right] - + *) type hypinfo = { @@ -202,7 +202,7 @@ type hypinfo = function can be provided to check the type of every free variable of the body of the hypothesis. *) val get_hypinfo :Term.constr -> l2r:bool -> ?check_type:(Term.types -> bool) -> (hypinfo -> Proof_type.tactic) -> Proof_type.tactic - + (** {2 Rewriting with bindings} The problem : Given a term to rewrite of type [H :forall xn ... x1, |