diff options
| author | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-30 11:30:53 +0200 |
| commit | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (patch) | |
| tree | cc39f942a75fd621633b1ac0999bbe4b3918fcfd /toplevel | |
| parent | 224d3b0e8be9b6af8194389141c9508504cf887c (diff) | |
| parent | 41e4725805588b3fffdfdc0cd5ee6859de1612b5 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
3 files changed, 11 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 0b0fd4ef16..75e8369222 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1120,7 +1120,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6909d89440..4ee3bc4745 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -48,6 +48,10 @@ let print_usage_channel co command = \n -compile f compile Coq file f.v (implies -batch)\ \n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ \n -quick quickly compile .v files to .vio files (skip proofs)\ +\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ +\n into fi.vo\ +\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ +\n proofs in each fi.vio\ \n\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a4ffae0fff..62e5f0a324 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -749,7 +749,11 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) -let vernac_require import qidl = +let vernac_require from import qidl = + let qidl = match from with + | None -> qidl + | Some ns -> List.map (Libnames.join_reference ns) qidl + in let qidl = List.map qualid_of_reference qidl in let modrefl = List.map Library.try_locate_qualified_library qidl in if Dumpglob.dump () then @@ -1884,7 +1888,7 @@ let interp ?proof locality poly c = | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set - | VernacRequire (export, qidl) -> vernac_require export qidl + | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t |