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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 19 |
3 files changed, 18 insertions, 9 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 24c3a5d9f1..f4c032e735 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -585,8 +585,8 @@ let is_inference_forced p evd ev = then let (loc, k) = evar_source ev evd in match k with - | ImplicitArg (_, _, b) -> b - | QuestionMark _ -> false + | Evar_kinds.ImplicitArg (_, _, b) -> b + | Evar_kinds.QuestionMark _ -> false | _ -> true else true with Not_found -> assert false @@ -683,7 +683,7 @@ let initial_select_evars with_goals = Typeclasses.is_class_evar evd evi) else (fun evd ev evi -> - (snd (Evd.evar_source ev evd) <> Evd.GoalEvar) + (snd (Evd.evar_source ev evd) <> Evar_kinds.GoalEvar) && Typeclasses.is_class_evar evd evi) let resolve_typeclass_evars debug m env evd with_goals split fail = diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index f1341762a2..a33b6b19bb 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -52,7 +52,7 @@ let instantiate n (ist,rawc) ido gl = gl let let_evar name typ gls = - let src = (dummy_loc,GoalEvar) in + let src = (dummy_loc,Evar_kinds.GoalEvar) in let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None nowhere) gls diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 61ffe599f6..e497581ed5 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -558,8 +558,13 @@ let subst_var_with_hole occ tid t = let rec substrec = function | GVar (_,id) as x -> if id = tid - then (decr occref; if !occref = 0 then x - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) + then + (decr occref; + if !occref = 0 then x + else + (incr locref; + GHole (make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true)))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -570,9 +575,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evd.QuestionMark(Evd.Define true)) -> - decr occref; if !occref = 0 then tc - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) -> + decr occref; + if !occref = 0 then tc + else + (incr locref; + GHole (make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true))) | c -> map_glob_constr_left_to_right substrec c in substrec t |