From 2f7d41425a4a75eec9a72123e0cc8541ed256163 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 12:16:11 +0000 Subject: [PATCH] Cosmetic changes. --- helm/ocaml/tactics/discriminationTactics.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 901540b6f..cf0db10e6 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -23,8 +23,6 @@ * http://cs.unibo.it/helm/. *) -open HelmLibraryObjects - let debug_print = fun _ -> () let rec injection_tac ~term = @@ -41,7 +39,7 @@ let rec injection_tac ~term = ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -97,7 +95,7 @@ and injection1_tac ~term ~i = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -219,7 +217,7 @@ let discriminate'_tac ~term = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -278,8 +276,8 @@ let discriminate'_tac ~term = C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(Logic.false_URI,0,[])) - else (C.MutInd(Logic.true_URI,0,[])) + then (C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[])) + else (C.MutInd(HelmLibraryObjects.Logic.true_URI,0,[])) in aux red_ty 1 ) constructor_list @@ -289,7 +287,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(Logic.false_URI,0,[]))) + ~term:(C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[]))) status in (match goals' with -- 2.39.2