diff options
| author | Enrico Tassi | 2015-10-06 16:43:50 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-10-08 09:51:13 +0200 |
| commit | 4a0fd14dcae807e0e681cfc14daca978cb4a36e9 (patch) | |
| tree | 05c168d43e4e6d7f1a68ce76fc7434c92304f455 /toplevel | |
| parent | 9ea8867a0fa8f2a52df102732fdc1a931c659826 (diff) | |
aux_file: export API to ease writing of a Proof Using annotator.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 72c800f0f1..6f1ed85e07 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1846,8 +1846,9 @@ let vernac_load interp fname = (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility *) -let interp ?proof locality poly c = + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let interp ?proof ~loc locality poly c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) @@ -1991,10 +1992,16 @@ let interp ?proof locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no" + | VernacProof (Some tac, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no"; + vernac_set_end_tac tac + | VernacProof (None, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes"; + vernac_set_used_variables l | VernacProof (Some tac, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes"; vernac_set_end_tac tac; vernac_set_used_variables l | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) @@ -2146,8 +2153,9 @@ let interp ?(verbosely=true) ?proof (loc,c) = Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> - if verbosely then Flags.verbosely (interp ?proof locality poly) c - else Flags.silently (interp ?proof locality poly) c; + if verbosely + then Flags.verbosely (interp ?proof ~loc locality poly) c + else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode end |