diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /plugins/xml/proof2aproof.ml | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/xml/proof2aproof.ml')
-rw-r--r-- | plugins/xml/proof2aproof.ml | 78 |
1 files changed, 0 insertions, 78 deletions
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml deleted file mode 100644 index 2d16190b..00000000 --- a/plugins/xml/proof2aproof.ml +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * The HELM Project / The EU MoWGLI Project *) -(* * University of Bologna *) -(************************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(* *) -(* Copyright (C) 2000-2004, HELM Team. *) -(* http://helm.cs.unibo.it *) -(************************************************************************) - -(* Note: we can not use the Set module here because we _need_ physical *) -(* equality and there exists no comparison function compatible with *) -(* physical equality. *) - -module S = - struct - let empty = [] - let mem = List.memq - let add x l = x::l - end -;; - -(* evar reduction that preserves some terms *) -let nf_evar sigma ~preserve = - let module T = Term in - let rec aux t = - if preserve t then t else - match T.kind_of_term t with - | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ - | T.Construct _ -> t - | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2) - | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2) - | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c) - | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c) - | T.App (c,l) -> - let c' = aux c in - let l' = Array.map aux l in - (match T.kind_of_term c' with - T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') - | T.Cast (he,_,_) -> - (match T.kind_of_term he with - T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') - | _ -> T.mkApp (c', l') - ) - | _ -> T.mkApp (c', l')) - | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> - aux (Evd.existential_value sigma (e,l)) - | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) - | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) - | T.Fix (ln,(lna,tl,bl)) -> - T.mkFix (ln,(lna,Array.map aux tl,Array.map aux bl)) - | T.CoFix(ln,(lna,tl,bl)) -> - T.mkCoFix (ln,(lna,Array.map aux tl,Array.map aux bl)) - in - aux -;; - -module ProofTreeHash = - Hashtbl.Make - (struct - type t = Proof_type.proof_tree - let equal = (==) - let hash = Hashtbl.hash - end) -;; - - -let extract_open_proof sigma pf = - (* Deactivated and candidate for removal. (Apr. 2010) *) - () - -let extract_open_pftreestate pts = - (* Deactivated and candidate for removal. (Apr. 2010) *) - () |