From 7248f6cccfcca2b0d59b244e8789590794aefc45 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 12 May 2008 12:27:25 +0000 Subject: - 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 --- contrib/interface/xlate.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9db1c7dc42..1095228b53 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2111,7 +2111,7 @@ let rec xlate_vernac = | VernacNop -> CT_proof_no_op | VernacComments l -> CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) - | VernacDeclareImplicits(true, id, _, opt_positions) -> + | VernacDeclareImplicits(true, id, opt_positions) -> CT_implicits (reference_to_ct_ID id, match opt_positions with @@ -2124,7 +2124,7 @@ let rec xlate_vernac = -> xlate_error "explication argument by rank is obsolete" | ExplByName id, _, _ -> CT_ident (string_of_id id)) l))) - | VernacDeclareImplicits(false, id, _, opt_positions) -> + | VernacDeclareImplicits(false, id, opt_positions) -> xlate_error "TODO: Implicit Arguments Global" | VernacReserve((_,a)::l, f) -> CT_reserve(CT_id_ne_list(xlate_ident a, -- cgit v1.2.3