diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-15 10:45:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a (patch) | |
| tree | aa6ed287eaa6759c6da083ff0a10c489784beba2 /proofs/clenv.mli | |
| parent | 63ae87d51456add79652b42b972d6be93b6119bc (diff) | |
Removing most nf_enter in tactics.
Now they are useless because all of the primitives are (should?) be
evar-insensitive.
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index f7ff4bed3..4bcd50591 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv + ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -62,9 +62,12 @@ val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (** unifies the concl of the goal with the type of the clenv *) -val clenv_unique_resolver : +val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv +val clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv + val clenv_dependent : clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv |