← Back to branch summary

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

« back to all changes in this revision

Viewing changes to toplevel/vernacentries.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
toplevel/vernacentries.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(*i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*)
 
9
(*i $Id: vernacentries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
10
10
 
11
11
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
12
12
 
370
370
        (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.")
371
371
 
372
372
let vernac_assumption kind l nl=
373
 
  if Pfedit.refining () then
374
 
    errorlabstrm ""
375
 
      (str "Cannot declare an assumption while in proof editing mode.");
376
373
  let global = fst kind = Global in
377
374
    List.iter (fun (is_coe,(idl,c)) ->
378
375
      if Dumpglob.dump () then
1113
1110
      pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
1114
1111
  | PrintAbout qid -> msg (print_about qid)
1115
1112
  | PrintImplicit qid -> msg (print_impargs qid)
1116
 
(*spiwack: prints all the axioms and section variables used by a term *)
1117
1113
  | PrintAssumptions (o,r) ->
 
1114
      (* Prints all the axioms and section variables used by a term *)
1118
1115
      let cstr = constr_of_global (smart_global r) in
1119
 
      let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
1120
 
        ~add_opaque:o cstr (Global.env ()) in
1121
 
      msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
 
1116
      let st = Conv_oracle.get_transp_state () in
 
1117
      let nassums = Assumptions.assumptions st ~add_opaque:o cstr in
 
1118
      msg (Printer.pr_assumptionset (Global.env ()) nassums)
1122
1119
 
1123
1120
let global_module r =
1124
1121
  let (loc,qid) = qualid_of_reference r in