diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 17:09:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-06 17:24:39 +0200 |
| commit | 521a7b96c8963428ca0ecb39a22f458bf603ccab (patch) | |
| tree | 4b96ec735f49ef1867348170b7432f9c7adb28bf /tactics/eqdecide.ml | |
| parent | 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c (diff) | |
Renaming goal-entering functions.
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 1c249c999..a43e99a7f 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -132,7 +132,7 @@ let match_eqdec c = (* /spiwack *) let solveArg eqonleft op a1 a2 tac = - Proofview.Goal.raw_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let rectype = pf_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let subtacs = @@ -144,7 +144,7 @@ let solveArg eqonleft op a1 a2 tac = let solveEqBranch rectype = Proofview.tclORELSE begin - Proofview.Goal.raw_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -171,7 +171,7 @@ let hd_app c = match kind_of_term c with let decideGralEquality = Proofview.tclORELSE begin - Proofview.Goal.raw_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = pf_nf_concl gl in match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app (pf_compute gl typ) in @@ -193,7 +193,7 @@ let decideGralEquality = let decideEqualityGoal = tclTHEN intros decideGralEquality let decideEquality rectype = - Proofview.Goal.raw_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let decide = mkGenDecideEqGoal rectype gl in (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) end @@ -202,7 +202,7 @@ let decideEquality rectype = (* The tactic Compare *) let compare c1 c2 = - Proofview.Goal.raw_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let rectype = pf_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) |