diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-25 17:39:18 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-25 17:39:18 +0000 |
| commit | 31dbba5f5c16f81c6dac2adaba46087da787ac12 (patch) | |
| tree | a3402adb697f4272a859028590ec0a905709327e /tactics/extratactics.ml4 | |
| parent | de5bd6a09e2323faf4ac4b7576d55c3d2cb94ba7 (diff) | |
Monomorphization (tactics)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16003 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1c9833571..4e22044d5 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -448,7 +448,7 @@ let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) let inTransitivity : bool * constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); + open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); subst_function = subst_transitivity_lemma; classify_function = (fun o -> Substitute o) } @@ -555,10 +555,10 @@ let subst_var_with_hole occ tid t = let locref = ref 0 in let rec substrec = function | GVar (_,id) as x -> - if id = tid + if id_eq id tid then (decr occref; - if !occref = 0 then x + if Int.equal !occref 0 then x else (incr locref; GHole (Loc.make_loc (!locref,0), @@ -575,7 +575,7 @@ let subst_hole_with_term occ tc t = let rec substrec = function | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) -> decr occref; - if !occref = 0 then tc + if Int.equal !occref 0 then tc else (incr locref; GHole (Loc.make_loc (!locref,0), @@ -654,7 +654,7 @@ END exception Found of tactic let rewrite_except h g = - tclMAP (fun id -> if id = h then tclIDTAC else + tclMAP (fun id -> if id_eq id h then tclIDTAC else tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) (Tacmach.pf_ids_of_hyps g) g |