diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-24 04:38:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f (patch) | |
| tree | edfad66c97aeea8b7e4aad4aba395aacb2175a3c /proofs | |
| parent | 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 (diff) | |
[api] Misctypes removal: tactic flags.
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 10 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 7 |
2 files changed, 8 insertions, 9 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 38ed63c23..544175c6d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,7 +54,7 @@ let clenv_cast_meta clenv = let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) -let clenv_pose_dependent_evars with_evars clenv = +let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then @@ -75,12 +75,12 @@ let check_tc evd = let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in (has_typeclass, !has_resolvable) -let clenv_refine with_evars ?(with_classes=true) clenv = +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> - let clenv = clenv_pose_dependent_evars with_evars clenv in + let clenv = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then let (has_typeclass, has_resolvable) = check_tc clenv.evd in @@ -105,10 +105,10 @@ open Unification let dft = default_unify_flags -let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter begin fun gl -> let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes clenv + clenv_refine ?with_evars ~with_classes clenv end (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 7c1e300b8..d17847842 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -13,12 +13,11 @@ open Clenv open EConstr open Unification -open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic +val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic -val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr |