diff options
| author | msozeau | 2008-05-12 12:27:25 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-12 12:27:25 +0000 |
| commit | 7248f6cccfcca2b0d59b244e8789590794aefc45 (patch) | |
| tree | 8979753245e2ff2ef183d37ba324f64c90b5d337 /contrib/interface | |
| parent | bba897d5fd964bef0aa10102ef41cee1ac5fc3bb (diff) | |
- 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
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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, |