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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** This file defines clausenv, which is a deprecated way to handle open terms
in the proof engine. This API is legacy. *)
open Constr
open Environ
open Evd
open EConstr
open Unification
open Tactypes
(** {6 The Type of Constructions clausale environments.} *)
type clausenv
val clenv_evd : clausenv -> Evd.evar_map
(* Ad-hoc primitives *)
val update_clenv_evd : clausenv -> evar_map -> clausenv
val clenv_strip_proj_params : clausenv -> clausenv
val clenv_refresh : env -> evar_map -> UnivGen.sort_context_set option -> clausenv -> clausenv
val clenv_arguments : clausenv -> metavariable list
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
(** type of clenv (instantiated) *)
val clenv_type : clausenv -> types
val mk_clenv_from : env -> evar_map -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n : env -> evar_map -> int -> EConstr.constr * EConstr.types -> clausenv
(** {6 linking of clenvs } *)
val clenv_instantiate : ?flags:unify_flags -> ?submetas:(metavariable * clbinding) list ->
metavariable -> clausenv -> (constr * types) -> clausenv
(** {6 Bindings } *)
(** bindings where the key is the position in the template of the
clenv (dependent or not). Positions can be negative meaning to
start from the rightmost argument of the template. *)
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
(** start with a clenv to refine with a given term with bindings *)
(** the arity of the lemma is fixed
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
val make_clenv_binding_apply :
env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
val make_clenv_binding :
env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
val clenv_push_prod : clausenv -> (metavariable * bool * clausenv) option
(** {6 Clenv tactics} *)
val unify : ?flags:unify_flags -> cv_pb:Conversion.conv_pb -> constr -> unit Proofview.tactic
val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
val case_pf : ?with_evars:bool ->
dep:bool -> (constr * types) -> unit Proofview.tactic
val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
(** {6 Pretty-print (debug only) } *)
val pr_clenv : clausenv -> Pp.t
module Internal :
sig
(** The legacy refiner. Do not use. *)
val refiner : clausenv -> unit Proofview.tactic
[@@ocaml.deprecated]
end
|