diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/toplevel.ml | 5 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 3 |
3 files changed, 6 insertions, 8 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 33f8e488ff..399134d115 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -237,13 +237,10 @@ let print_toplevel_error exc = (if is_pervasive_exn exc then (mt ()) else locstrm) ++ Cerrors.explain_exn exc -let is_term s = - if !Options.v7 then s="." else s=";" - (* Read the input stream until a dot is encountered *) let parse_to_dot = let rec dot st = match Stream.next st with - | ("", c) when is_term c -> () + | ("", ".") -> () | ("EOI", "") -> raise End_of_input | _ -> dot st in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1d2ccecbb0..2b3b05b302 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -159,7 +159,7 @@ let show_intro all = (* "Print" commands *) let print_path_entry (s,l) = - (str s ++ tbrk (0,2) ++ str (string_of_dirpath l)) + (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l)) let print_loadpath () = let l = Library.get_full_load_path () in @@ -703,7 +703,7 @@ let vernac_syntactic_definition id c = function | None -> syntax_definition id c | Some n -> let l = list_tabulate (fun _ -> (CHole (dummy_loc),None)) n in - let c = CApp (dummy_loc,(false,c),l) in + let c = CApp (dummy_loc,(None,c),l) in syntax_definition id c let vernac_declare_implicits locqid = function @@ -1172,7 +1172,7 @@ let interp c = match c with | VernacEndSegment id -> vernac_end_segment id - | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs + | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e03658cfd4..266e6c0942 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -183,7 +183,8 @@ type vernac_expr = | VernacScheme of (identifier * bool * reference * sort_expr) list (* Gallina extensions *) - | VernacRecord of identifier with_coercion * simple_binder list + | VernacRecord of bool (* = Record or Structure *) + * identifier with_coercion * simple_binder list * constr_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSegment of identifier |