From f17da39739c49297bf435896c8cb4e3ac83b95a6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 12 Jan 2006 10:29:26 +0000 Subject: [PATCH] Dead code removed. --- helm/ocaml/acic_content/acic2content.ml | 1 - helm/ocaml/cic_unification/cicRefine.ml | 2 +- helm/ocaml/library/librarySync.ml | 4 ++-- helm/ocaml/tactics/equalityTactics.ml | 9 +-------- helm/ocaml/tactics/fourierR.ml | 10 +++------- helm/ocaml/tactics/proofEngineReduction.ml | 20 +++++++++----------- 6 files changed, 16 insertions(+), 30 deletions(-) diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml index 8f3b13cfd..ed4eafb4e 100644 --- a/helm/ocaml/acic_content/acic2content.ml +++ b/helm/ocaml/acic_content/acic2content.ml @@ -576,7 +576,6 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = K.ArgProof {body with K.proof_name = name; K.proof_context=context} in List.map2 build_proof patterns name_and_arities in - let teid = get_id te in let context,term = (match build_subproofs_and_args diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index f03752d10..f01ecf785 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -853,7 +853,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t and avoid_double_coercion subst metasenv ugraph t ty = match t with - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index fe631edd2..922955aa0 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -50,7 +50,7 @@ let merge_coercions obj = C.Lambda (name, aux so, aux dest) | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> let source_carr = CoercGraph.source_of c2 in let tgt_carr = CoercGraph.target_of c1 in @@ -180,7 +180,7 @@ let index_obj = let add_single_obj uri obj ~basedir = let obj = - if List.mem `Generated (CicUtil.attributes_of_obj obj) && + if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) then merge_coercions obj diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 8304d7bb1..b3dc1bb9e 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -67,14 +67,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit | _::tl -> find_hyp (n+1) tl in let arg,gty = find_hyp 1 context in - let last_hyp_name_of_status (proof,goal) = - let curi, metasenv, pbo, pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - match context with - (Some (Cic.Name s,_))::_ -> s - | _ -> assert false - in - let dummy = "dummy" in + let dummy = "dummy" in Some arg,false, (fun ~term typ -> Tacticals.seq diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 5418e1149..8b910bded 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -196,8 +196,8 @@ let rational_of_const = rational_of_term;; *) let fails f a = try - let tmp = (f a) in - false + ignore (f a); + false with _-> true ;; @@ -662,11 +662,7 @@ let tac_zero_inf_false gl (n,d) = apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status else apply_tactic (Tacticals.then_ - ~start:( mk_tactic (fun status -> - let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status)) + ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt))) ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 755a09854..cc5af63ae 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -695,18 +695,16 @@ let simpl context = in reduceaux context [] body' | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - let tl' = List.map (reduceaux context []) tl in - reduceaux context tl' body' + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux context tl' body' | t -> t in (match decofix (CicReduction.whd context term) with -- 2.39.2