Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7

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