← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to proofs/proof_trees.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
proofs/proof_trees.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *)
 
10
 
 
11
open Closure
 
12
open Util
 
13
open Names
 
14
open Nameops
 
15
open Term
 
16
open Termops
 
17
open Sign
 
18
open Evd
 
19
open Environ
 
20
open Evarutil
 
21
open Decl_expr
 
22
open Proof_type
 
23
open Tacred
 
24
open Typing
 
25
open Libnames
 
26
open Nametab
 
27
 
 
28
(*
 
29
let is_bind = function
 
30
  | Tacexpr.Cbindings _ -> true
 
31
  | _ -> false
 
32
*)
 
33
 
 
34
(* Functions on goals *)
 
35
 
 
36
let mk_goal hyps cl extra = 
 
37
  { evar_hyps = hyps; evar_concl = cl; 
 
38
    evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
 
39
    evar_body = Evar_empty; evar_extra = extra }
 
40
 
 
41
(* Functions on proof trees *)
 
42
 
 
43
let ref_of_proof pf =
 
44
  match pf.ref with
 
45
    | None -> failwith "rule_of_proof"
 
46
    | Some r -> r
 
47
 
 
48
let rule_of_proof pf =
 
49
  let (r,_) = ref_of_proof pf in r
 
50
 
 
51
let children_of_proof pf = 
 
52
  let (_,cl) = ref_of_proof pf in cl
 
53
                                    
 
54
let goal_of_proof pf = pf.goal
 
55
 
 
56
let subproof_of_proof pf = match pf.ref with
 
57
  | Some (Nested (_,pf), _) -> pf
 
58
  | _ -> failwith "subproof_of_proof"
 
59
 
 
60
let status_of_proof pf = pf.open_subgoals
 
61
 
 
62
let is_complete_proof pf = pf.open_subgoals = 0
 
63
 
 
64
let is_leaf_proof pf = (pf.ref = None)
 
65
 
 
66
let is_tactic_proof pf = match pf.ref with
 
67
  | Some (Nested (Tactic _,_),_) -> true
 
68
  | _ -> false
 
69
 
 
70
 
 
71
let pf_lookup_name_as_renamed env ccl s =
 
72
  Detyping.lookup_name_as_renamed env ccl s
 
73
 
 
74
let pf_lookup_index_as_renamed env ccl n =
 
75
  Detyping.lookup_index_as_renamed env ccl n
 
76
 
 
77
(* Functions on rules (Proof mode) *) 
 
78
 
 
79
let is_dem_rule  = function
 
80
    Decl_proof _  -> true
 
81
  | _ -> false
 
82
 
 
83
let is_proof_instr = function
 
84
    Nested(Proof_instr (_,_),_) -> true
 
85
  | _ -> false
 
86
 
 
87
let is_focussing_command = function
 
88
    Decl_proof b -> b 
 
89
  | Nested (Proof_instr (b,_),_) -> b 
 
90
  | _ -> false   
 
91
 
 
92
 
 
93
(*********************************************************************)
 
94
(*                  Pretty printing functions                        *)
 
95
(*********************************************************************)
 
96
 
 
97
open Pp
 
98
 
 
99
let db_pr_goal g =
 
100
  let env = evar_env g in
 
101
  let penv = print_named_context env in
 
102
  let pc = print_constr_env env g.evar_concl in
 
103
  str"  " ++ hv 0 (penv ++ fnl () ++
 
104
                   str "============================" ++ fnl ()  ++
 
105
                   str" "  ++ pc) ++ fnl ()
 
106