aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_trees.ml
diff options
context:
space:
mode:
authorglondu2009-09-17 15:58:14 +0000
committerglondu2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /proofs/proof_trees.ml
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_trees.ml')
-rw-r--r--proofs/proof_trees.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 2e2f23065a..b5f46d7887 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -33,8 +33,8 @@ let is_bind = function
(* Functions on goals *)
-let mk_goal hyps cl extra =
- { evar_hyps = hyps; evar_concl = cl;
+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_extra = extra }
@@ -48,9 +48,9 @@ let ref_of_proof pf =
let rule_of_proof pf =
let (r,_) = ref_of_proof pf in r
-let children_of_proof pf =
+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
@@ -74,7 +74,7 @@ let pf_lookup_name_as_renamed 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) *)
+(* Functions on rules (Proof mode) *)
let is_dem_rule = function
Decl_proof _ -> true
@@ -85,9 +85,9 @@ let is_proof_instr = function
| _ -> false
let is_focussing_command = function
- Decl_proof b -> b
- | Nested (Proof_instr (b,_),_) -> b
- | _ -> false
+ Decl_proof b -> b
+ | Nested (Proof_instr (b,_),_) -> b
+ | _ -> false
(*********************************************************************)