diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 6438f5855..593ef0b32 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -694,27 +694,6 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = - let rec aux p vars = - let _,subst = - List.fold_left (fun (n,l) var -> - let t = match var with - | Anonymous,_ -> l - | Name id, ProofVar -> (id,mkRel n)::l - | Name id, SectionVar id' -> (id,mkVar id')::l in - (n+1,t)) (p,[]) vars - in replace_vars (List.rev subst) - in aux 1 - -let rec rebind id1 id2 = function - | [] -> [Name id2,SectionVar id1] - | (na,k as x)::l -> - if na = Name id1 then (Name id2,k)::l else - let l' = rebind id1 id2 l in - if na = Name id2 then (Anonymous,k)::l' else x::l' - -let add_proof_var id vl = (Name id,ProofVar)::vl - let proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n |