diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /proofs/proof_trees.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'proofs/proof_trees.ml')
-rw-r--r-- | proofs/proof_trees.ml | 107 |
1 files changed, 0 insertions, 107 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml deleted file mode 100644 index 8fe1a4c2..00000000 --- a/proofs/proof_trees.ml +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: proof_trees.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - -open Closure -open Util -open Names -open Nameops -open Term -open Termops -open Sign -open Evd -open Environ -open Evarutil -open Decl_expr -open Proof_type -open Tacred -open Typing -open Libnames -open Nametab - -(* -let is_bind = function - | Tacexpr.Cbindings _ -> true - | _ -> false -*) - -(* Functions on goals *) - -let mk_goal hyps cl extra = - { evar_hyps = hyps; evar_concl = cl; - evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); - evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar); - evar_extra = extra } - -(* Functions on proof trees *) - -let ref_of_proof pf = - match pf.ref with - | None -> failwith "rule_of_proof" - | Some r -> r - -let rule_of_proof pf = - let (r,_) = ref_of_proof pf in r - -let children_of_proof pf = - let (_,cl) = ref_of_proof pf in cl - -let goal_of_proof pf = pf.goal - -let subproof_of_proof pf = match pf.ref with - | Some (Nested (_,pf), _) -> pf - | _ -> failwith "subproof_of_proof" - -let status_of_proof pf = pf.open_subgoals - -let is_complete_proof pf = pf.open_subgoals = 0 - -let is_leaf_proof pf = (pf.ref = None) - -let is_tactic_proof pf = match pf.ref with - | Some (Nested (Tactic _,_),_) -> true - | _ -> false - - -let pf_lookup_name_as_displayed env ccl s = - Detyping.lookup_name_as_displayed env ccl s - -let pf_lookup_index_as_renamed env ccl n = - Detyping.lookup_index_as_renamed env ccl n - -(* Functions on rules (Proof mode) *) - -let is_dem_rule = function - Decl_proof _ -> true - | _ -> false - -let is_proof_instr = function - Nested(Proof_instr (_,_),_) -> true - | _ -> false - -let is_focussing_command = function - Decl_proof b -> b - | Nested (Proof_instr (b,_),_) -> b - | _ -> false - - -(*********************************************************************) -(* Pretty printing functions *) -(*********************************************************************) - -open Pp - -let db_pr_goal g = - let env = evar_env g in - let penv = print_named_context env in - let pc = print_constr_env env g.evar_concl in - str" " ++ hv 0 (penv ++ fnl () ++ - str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () - |