- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to

  change the default pretty-printing to use Π, λ instead of
  forall and fun (and allow "," as well as "=>" for "fun" to be more
  consistent with the standard forall and exists syntax). Parsing allows
  theses new forms too, even if not in -unicode, and does not make Π or
  λ keywords. As usual, criticism and suggestions are welcome :)
  Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
  for tactics. 
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
  combination.
- Backtrack on [Enriching] modifier, now used exclusively in the 
  implementation of implicit arguments.


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

3 files changed, 7 insertions, 5 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a4dee4b6e..d09a87dc6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -253,7 +253,9 @@ let parse_args is_ide =
     | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
     | "-emacs-U" :: rem -> Flags.print_emacs := true; 
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-	  
+	
+    | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+
     | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
     | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e9b49e7e8..c705d0287 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -681,9 +681,9 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits local r e = function
+let vernac_declare_implicits local r = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (global_with_alias r) e
+      Impargs.declare_manual_implicits local (global_with_alias r) false
 	(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
   | None -> 
       Impargs.declare_implicits local (global_with_alias r)
@@ -1266,7 +1266,7 @@ let interp c = match c with
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (local,qid,e,l) ->vernac_declare_implicits local qid e l
+  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 16589805f..986c63c0b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -290,7 +290,7 @@ type vernac_expr =
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
-  | VernacDeclareImplicits of locality_flag * lreference * bool *
+  | VernacDeclareImplicits of locality_flag * lreference * 
       (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list