diff options
| author | letouzey | 2012-05-29 11:08:26 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:26 +0000 |
| commit | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (patch) | |
| tree | 8a30a206d390e1b7450889189596641e5026ee46 /proofs | |
| parent | 3854ae16ffbaf56b90fbb85bcce3d92cd65ea6a6 (diff) | |
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index c4df5721fa..cfe69c7054 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -319,7 +319,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = if occur_meta ty then fold clenv (mvs@[mv]) else let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in + new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/goal.ml b/proofs/goal.ml index 37bb96de73..cef43c443e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -498,7 +498,7 @@ module V82 = struct Evd.evar_filter = List.map (fun _ -> true) (Environ.named_context_of_val hyps); Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Pp.dummy_loc,Evd.GoalEvar); + Evd.evar_source = (Pp.dummy_loc,Evar_kinds.GoalEvar); Evd.evar_candidates = None; Evd.evar_extra = extra } in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 320e01f4fc..2f3f58dc30 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -179,7 +179,7 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac let solve_by_implicit_tactic env sigma (evk,args) = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with - | Some tac, (ImplicitArg _ | QuestionMark _) + | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> |