diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
| commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
| tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 | |
| parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
| parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) | |
Merge commit 'upstream/8.3+dfsg' into experimental/master
107 files changed, 1286 insertions, 2448 deletions
@@ -110,6 +110,7 @@ Specification language - Binders given before ":" in lemmas and in definitions built by tactics are now automatically introduced (possible source of incompatibility that can be resolved by invoking "Unset Automatic Introduction"). +- New support for multiple implicit arguments signatures per reference. Module system @@ -139,6 +140,12 @@ Extraction dangerous for the complexity. In particular many eta-expansions at the top of functions body are now avoided, clever partial applications will likely be preserved, let-ins are almost always kept, etc. +- In the same spirit, auto-inlining is now disabled by default, except for + induction principles, since this feature was producing more frequently + weird code than clear gain. The previous behavior can be restored via + "Set Extraction AutoInline". +- Unicode characters in identifiers are now transformed into ascii strings + that are legal in Ocaml and other languages. - Harsh support of module extraction to Haskell and Scheme: module hierarchy is flattened, module abbreviations and functor applications are expanded, module types and unapplied functors are discarded. @@ -190,11 +197,11 @@ Vernacular commands illustration of wrong commands. - Most commands referring to constant (e.g. Print or About) now support referring to the constant by a notation string. -- Made generation of boolean equality automatic for datatypes (use - "Unset Boolean Equality Schemes" for deactivation). -- Made support for automatic generation of case analysis schemes and - congruence schemes available to user (governed by options "Unset - Case Analysis Schemes" and "Unset Congruence Schemes"). +- New option "Boolean Equality Schemes" to make generation of boolean + equality automatic for datatypes (together with option "Decidable + Equality Schemes", this replaces deprecated option "Equality Scheme"). +- Made support for automatic generation of case analysis schemes available + to user (governed by option "Set Case Analysis Schemes"). - New command "(Global?) Generalizable [All|No] Variable(s)? ident(s)?" to declare which identifiers are generalizable in `{} and `() binders. - New command "Print Opaque Dependencies" to display opaque constants in @@ -205,6 +212,8 @@ Vernacular commands - Syntax of Implicit Type now supports more than one block of variables of a given type. - Command "Canonical Structure" now warns when it has no effects. +- Commands of the form "Set X" or "Unset X" now support "Local" and "Global" + prefixes. Library diff --git a/COMPATIBILITY b/COMPATIBILITY index 09b72e92..4cc8b589 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -20,35 +20,33 @@ incompatibilities listed below must however be treated manually. Syntax - The word "by" is now a keyword and can no longer be used as an identifier. - [Semantics, IEEE754] Type inference -- Many changes in using classes. [ATBR] +- Many changes in using classes. Library - New identifiers of the library can hide identifiers. This can be solved by changing the order of Require or by qualifying the - identifier with the name of its module. [Stalmarck] + identifier with the name of its module. - Reorganisation of library (esp. FSets, Sorting, Numbers) may have - moved or removed names around. [FundamentalArithmetics, CoLoR, - Icharate, AMM11262, FSets, FingerTree] + changed or removed names around. - Infix notation "++" has now to be set at level 60. [LinAlg] -- When using Program (refl_equal and Vnil have maximal implicit - arguments, lemmas about measure have a different form, ...). +- When using the Programs library or any feature that uses it, + (lemmas about measure have a different form, ...). Tactics - The synchronization of introduction names and quantified hypotheses names may exceptionally lead to different names in "induction" - (usually a name with lower index is required). [Automata] + (usually a name with lower index is required). - More checks in some commands (e.g. in Hint) may lead to forbid some - meaningless part of them. [CoLoR] + meaningless part of them. - When rewriting using setoid equality, the default equality found - might be different. [CoRN] + might be different. @@ -6,7 +6,7 @@ Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) Pierre Courtieu and Julien Forest, CNAM (plugins/funind) - Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) + Claudio Sacerdoti Coen, HELM, University of Bologna (plugins/xml) Pierre Corbineau, Radbout University, Nijmegen (declarative mode) John Harrison, University of Cambridge (csdp wrapper) @@ -15,8 +15,8 @@ WHAT DO YOU NEED ? ppc) and FreeBSD. Automated tests are run under many, many different architectures under GNU/Linux. - Naturally, Coq will run faster on an architecture where OCaml can - compile to native code, rather than only bytecode. At time of + Naturally, Coq will run faster on an architecture where Objective Caml + can compile to native code, rather than only bytecode. At time of writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, HPPA and StrongArm. See http://caml.inria.fr/ocaml/portability.en.html for details. @@ -41,11 +41,13 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.3 yourself, you need: - - Objective Caml version 3.09.3 or later + - Objective Caml version 3.10.2 or later (available at http://caml.inria.fr/) - For Ocaml version >= 3.10.0, you also need to install camlp5 - (version <= 4.08, or 5.01 transitional) + For Objective Caml version >= 3.10.0, you also need to install + camlp5 (use "transitional" mode and choose a version compatible + with the corresponding version of Objective Caml, however + avoiding version 5.00) - GNU Make version 3.81 or later @@ -73,9 +75,6 @@ WHAT DO YOU NEED ? - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details - By FTP, Coq comes as a single compressed tar-file. You have - probably already decompressed it if you are reading this document. - QUICK INSTALLATION PROCEDURE. ============================= @@ -89,7 +88,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.09.3 (or later) +1- Check that you have the Objective Caml compiler version 3.10.2 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. @@ -99,23 +98,16 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). bigger), you will also need the "ocamlopt" (or its native code version "ocamlopt.opt") command. -2- Check that you have Camlp4 installed on your - computer and that the command "camlp4" lies in a directory which +2- If using Ocaml >= 3.10, check that you have Camlp5 installed on your + computer and that the command "camlp5" lies in a directory which is present in your $PATH environment variable path. - (You need Camlp4 in both bytecode and native versions if - your platform supports it). - - Note: in the latest ocaml distributions, camlp4 comes with ocaml so - you do not have to check this point anymore. + (You need Camlp5 in transitional mode and in both bytecode and + native versions if your platform supports it). -3- The uncompression and un-tarring of the distribution file gave birth - to a directory named "coq-8.xx". You can rename this directory and put - it wherever you want. Just keep in mind that you will need some spare - space during the compilation (reckon on about 50 Mb of disk space - for the whole system in native-code compilation). Once installed, the - binaries take about 14 Mb, and the library about 9 Mb. +2- You will need about 400Mo free on your disk to compile Coq in full + with its standard library and documentation. -4- First you need to configure the system. It is done automatically with +3- First you need to configure the system. It is done automatically with the command: ./configure <options> @@ -209,7 +201,7 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS. binaries will reside in the subdirectory bin/. If you want to compile the sources for debugging (i.e. with the option - -g of the Caml compiler) then add the -debug option at configuration + -g of the ocaml compiler) then add the -debug option at configuration step : ./configure -debug <other options> @@ -324,7 +316,7 @@ MOVING BINARIES OR LIBRARY. DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. ====================================================== - Some bytecode executables of Coq use the OCaml runtime, which dynamically + Some bytecode executables of Coq use the ocaml runtime, which dynamically loads a shared library (.so or .dll). When it is not installed properly, you can get an error message of this kind: @@ -337,12 +329,12 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. the command a limited number of times in a controlled environment (e.g. during compilation of binary packages); - install dllcoqrun.so in a location listed in the file ld.conf that is in - the directory of the standard library of OCaml; + the directory of the standard library of Objective Caml; - recompile your bytecode executables after reconfiguring the location of of the shared library: ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ... where <path> is the directory where the dllcoqrun.so is installed; - - (not recommended) compile bytecode executables with a custom OCaml + - (not recommended) compile bytecode executables with a custom ocaml runtime by using: ./configure -custom ... be aware that stripping executables generated this way, or performing diff --git a/INSTALL.ide b/INSTALL.ide index 757d8354..e99002f0 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -23,10 +23,10 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. REQUIREMENT: - - OCaml >= 3.09.3 with native threads support. + - OCaml >= 3.10.2 with native threads support. - make world must succeed. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. - The official supported version is at least 2.8.x. + The official supported version is at least 2.10.x. You may still compile CoqIde with older versions and use all features. Run diff --git a/INSTALL.macosx b/INSTALL.macosx index cc1317b1..0750064d 100644 --- a/INSTALL.macosx +++ b/INSTALL.macosx @@ -1,20 +1,4 @@ -INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X ------------------------------------------------------------------------- +INSTALLATION PROCEDURE FOR THE PRECOMPILED VERSION OF COQ SYSTEM UNDER MACOS X +------------------------------------------------------------------------------ -You can also use fink, or the MacOS X package prepared by the Coq -team. To use the MacOS X package,: - -1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer) - or coq-8.1-macosx-i386.dmg (for Pentium-based computer). - -2) Double-click on its icon; it mounts a disk volume named "Coq V8.1". - -3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the - installer (you'll need administrator permissions). - -4) Coq installs in /usr/local/bin, which should be in your PATH, and - can be used from a Terminal window: the interactive toplevel is - named coqtop and the compiler is coqc. - -If you have any trouble with this installation, please contact: -coq-bugs@pauillac.inria.fr. +See up-to-date informations on http://coq.inria.fr/download. @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 13184 2010-06-23 09:19:15Z notin $ +# $Id: Makefile 13540 2010-10-13 19:53:28Z notin $ # Makefile for Coq @@ -220,6 +220,7 @@ docclean: rm -f doc/common/version.tex rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/*.eps doc/refman/Reference-Manual.html rm -f doc/coq.tex + rm -f doc/refman/styles.hva doc/refman/cover.html archclean: clean-ide cleantheories rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) diff --git a/Makefile.build b/Makefile.build index 4a7354e4..8af5be00 100644 --- a/Makefile.build +++ b/Makefile.build @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile.build 13324 2010-07-24 19:21:23Z glondu $ +# $Id: Makefile.build 13477 2010-09-30 16:50:00Z vgross $ # Makefile for Coq @@ -340,14 +340,6 @@ install-ide-info: $(MKDIR) $(FULLIDELIB) $(INSTALLLIB) ide/FAQ $(FULLIDELIB) -# IM files - -IMFILES=$(addprefix ide/uim/, coqide.scm coqide-rules.scm coqide-custom.scm) - -install-im: - $(INSTALLLIB) $(IMFILES) $(UIMSCRIPTDIR) - uim-module-manager --register coqide - ########################################################################### # tests ########################################################################### @@ -716,7 +708,7 @@ ifeq ($(CHECKEDOUT),git) if test -x "`which git`"; then \ LANG=C; export LANG; \ GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname --fqdn); \ + GIT_HOST=$$(hostname -f); \ GIT_PATH=$$(pwd); \ (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ diff --git a/Makefile.doc b/Makefile.doc index 56daaa85..4c6e209f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -127,7 +127,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html - $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html + -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -185,41 +185,33 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -ifdef QUICK -doc/stdlib/index-body.html: - - rm -rf doc/stdlib/html - $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ - -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html +ifeq ($(QUICK),1) +doc/stdlib/html/genindex.html: else -doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) +doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) +endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ + $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html -endif + mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index ./doc/stdlib/make-library-index doc/stdlib/index-list.html -doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html - cat doc/stdlib/index-list.html > $@ - sed -n -e '/<table>/,/<\/table>/p' doc/stdlib/index-body.html >> $@ - cat doc/stdlib/index-trailer.html >> $@ +doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html + cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@ + cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@ ### Standard library (light version, full version is definitely too big) ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ else -doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ +doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ @@ -27,8 +27,7 @@ CHANGES. AVAILABILITY. ============= - Coq is available at http://coq.inria.fr, or, for older versions at - ftp://ftp.inria.fr/INRIA/LogiCal/coq. + Coq is available at http://coq.inria.fr/download. THE COQ CLUB. @@ -38,7 +37,7 @@ THE COQ CLUB. discuss questions about the Coq system and related topics. The submission address is: - coq-club@coq.inria.fr + coq-club@inria.fr The topics to be discussed in the club should include: @@ -53,13 +52,10 @@ THE COQ CLUB. * theoretical questions about typed lambda-calculi which are closely related to Coq. - To be added to, or removed from, the mailing list, please write to: - - coq-club-request@coq.inria.fr - - Please use also this address for any questions/suggestions about the - Coq Club. It might sometimes take a few days before your messages get - forwarded. + To be added to, or removed from, the mailing list, go to + https://sympa-roc.inria.fr/wws/info/coq-club or write to + sympa@inria.fr with subject either "subscribe coq-club" or + "unsubscribe coq-club". List is moderated for non-subscribers. BUGS REPORT. @@ -67,8 +63,8 @@ BUGS REPORT. Send your bug reports by filling a form at - http://logical.saclay.inria.fr/coq-bugs + http://coq.inria.fr/bugs/ - To be effective, bug reports should mention the Caml version used - to compile and run Coq, the Coq version (coqtop -v), the configuration - used, and include a complete source example leading to the bug. + To be effective, bug reports should mention the Coq version (coqtop -v), + the configuration used, and include a complete source example + leading to the bug. @@ -20,12 +20,12 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3. + 1- Install ocaml for Windows (MinGW port), at least version 3.10.2. See: http://caml.inria.fr 2- Install a shell environment with at least: - a C compiler (gcc), - - the GNU make utility + - the GNU make utility (version >= 3.81) The Cygwin environment is well suited for compiling Coq (official packages are made using Cygwin) See: @@ -43,9 +43,9 @@ COMPILATION. make world make install - 5- Though not nescessary, you can find useful: + 5- Though not necessary, you can find useful: - Windows version of (X)Emacs: it is a powerful environment for - developpers with coloured syntax, modes for compilation and debug, + developers with colored syntax, modes for compilation and debug, and many more. It is free. See: http://www.gnu.org/software. - Windows subversion client (very useful if you have access to the Coq archive). @@ -55,6 +55,7 @@ "tactics/rewrite.ml4": use_grammar <plugins/**/*.ml4>: use_grammar +"plugins/subtac/g_subtac.ml4": use_extend ## sub-directory inclusion diff --git a/checker/declarations.ml b/checker/declarations.ml index 699f6c90..0deb80a2 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -580,7 +580,7 @@ let update_delta_resolver resolver1 resolver2 = Equiv (solve_delta_kn resolver2 kn) in Deltamap.add key new_hint res | _ -> Deltamap.add key hint res - with not_found -> + with Not_found -> Deltamap.add key hint res in Deltamap.fold apply_res resolver1 empty_delta_resolver diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 23ba4893..81154cba 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -238,15 +238,15 @@ and check_with_aux_mod env mtb with_decl mp = | Reduction.NotConvertible -> error_with_incorrect l and check_module_type env mty = - let _ = check_modtype env mty.typ_expr mty.typ_mp in () + let _ = check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in () and check_module env mp mb = match mb.mod_expr, mb.mod_type with | None,mtb -> - let _ = check_modtype env mtb mb.mod_mp in () + let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, mtb when mtb==mexpr -> - let _ = check_modtype env mtb mb.mod_mp in () + let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, _ -> let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in diff --git a/checker/reduction.ml b/checker/reduction.ml index 9f7dec28..d040c3db 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -154,7 +154,8 @@ type conv_pb = let sort_cmp univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible | (Prop c1, Type u) -> (match pb with CUMUL -> () diff --git a/config/Makefile.template b/config/Makefile.template index 74ec9580..8864f52d 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -138,9 +138,6 @@ STRIP=STRIPCOMMAND # CoqIde (no/byte/opt) HASCOQIDE=COQIDEOPT -# IM files -UIMSCRIPTDIR=UIMSCRIPTPATH - # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE @@ -6,7 +6,7 @@ # ################################## -VERSION=8.3-rc1 +VERSION=8.3 VOMAGIC=08300 STATEMAGIC=58300 DATE=`LANG=C date +"%B %Y"` @@ -67,8 +67,6 @@ usage () { printf "\tSpecifies whether or not to use dynamic loading of native code\n" echo "-coqide (opt|byte|no)" printf "\tSpecifies whether or not to compile Coqide\n" - echo "-uim-script-path" - printf "\tSpecifies where uim's .scm files are installed\n" echo "-browser <command>" printf "\tUse <command> to open URL %%s\n" echo "-with-doc (yes|no)" @@ -248,9 +246,6 @@ while : ; do -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) force_caml_version_spec=yes force_caml_version=yes;; - -uim-script-path) - uim_script_path=$2 - shift;; *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;; esac shift @@ -328,8 +323,8 @@ MAKE=`which make` if [ "$MAKE" != "" ]; then MAKEVERSION=`$MAKE -v | head -1` case $MAKEVERSION in - "GNU Make 3.81") - echo "You have GNU Make 3.81. Good!";; + "GNU Make 3.8"[12]) + echo "You have GNU Make >= 3.81. Good!";; *) OK="no" if [ -x ./make ]; then @@ -416,12 +411,12 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012]) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.09.3 or later." + echo " You need Objective-Caml 3.10.2 or later." echo " Configuration script failed!" exit 1 fi;; @@ -446,12 +441,6 @@ case $ARCH in CAMLLIB=`"$CAMLC" -where` esac -# We need to set a special flag for OCaml 3.07 -case $CAMLVERSION in - 3.07*) - cflags="$cflags -DOCAML_307";; -esac - if [ "$coq_debug_flag" = "-g" ]; then case $CAMLTAG in OCAML31*) @@ -535,7 +524,8 @@ else fi if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then - echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK." + echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK" + echo "(depending also on your ocaml version)." echo "Configuration script failed!" exit 1 fi @@ -652,15 +642,6 @@ case $COQIDE in no) LABLGTKINCLUDES="";; esac -if which uim-fep; then - for cand in i"$uim_script_path" /usr/local/share/uim/ /usr/share/uim/; do - if [ -f "$cand/loader.scm" ]; then - UIMSCRIPTDIR=$cand - break - fi - done -fi - # strip command case $ARCH in @@ -1100,7 +1081,6 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ -e "s|WITHDOCOPT|$with_doc|" \ -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \ - -e "s|UIMSCRIPTPATH|$UIMSCRIPTDIR|" \ "$config_template" > "$config_file" chmod a-w "$config_file" @@ -1114,4 +1094,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 13372 2010-08-06 08:36:16Z notin $ +# $Id: configure 13552 2010-10-14 14:02:46Z notin $ diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html new file mode 100644 index 00000000..2b4e0de0 --- /dev/null +++ b/doc/common/styles/html/coqremote/footer.html @@ -0,0 +1,43 @@ +<div id="sidebarWrapper"> +<div id="sidebar"> + +<div class="block"> +<h2 class="title">Navigation</h2> +<div class="content"> + +<ul class="menu"> + +<li class="leaf">Standard Library + <ul class="menu"> + <li><a href="index.html">Table of contents</a></li> + <li><a href="genindex.html">Index</a></li> + </ul> +</li> + +</ul> + +</div> +</div> + +</div> +</div> + + +</div> + +<div id="footer"> +<div id="nav-footer"> + <ul class="links-menu-footer"> + <li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li> + </ul> + +</div> +</div> + +</div> + +</body> +</html> + diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html new file mode 100644 index 00000000..025e1d3a --- /dev/null +++ b/doc/common/styles/html/coqremote/header.html @@ -0,0 +1,49 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> + +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> +<title>Standard Library | The Coq Proof Assistant</title> + +<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style> + +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style> + +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> + +</head> + +<body> + +<div id="container"> +<div id="headertop"> +<div id="nav"> + <ul class="links-menu"> + <li><a href="http://coq.inria.fr/" class="active">Home</a></li> + + <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> + <li><a href="http://coq.inria.fr/download">Get Coq</a></li> + <li><a href="http://coq.inria.fr/documentation">Documentation</a></li> + <li><a href="http://coq.inria.fr/community">Community</a></li> + </ul> +</div> +</div> + +<div id="header"> + +<div id="logoWrapper"> + +<div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a> +</div> +<div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a> +</div> + +</div> +</div> + +<div id="content"> + diff --git a/doc/stdlib/index-trailer.html b/doc/common/styles/html/simple/footer.html index 308b1d01..308b1d01 100644 --- a/doc/stdlib/index-trailer.html +++ b/doc/common/styles/html/simple/footer.html diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html new file mode 100644 index 00000000..14d2f988 --- /dev/null +++ b/doc/common/styles/html/simple/header.html @@ -0,0 +1,13 @@ +<!DOCTYPE html + PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> + +<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> +<link rel="stylesheet" href="coqdoc.css" type="text/css"/> +<title>The Coq Standard Library</title> +</head> + +<body> + diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7a24846b..7ee85fe8 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -1,17 +1,5 @@ -<!DOCTYPE html - PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" - "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> -<link rel="stylesheet" href="css/context.css" type="text/css"/> -<title>The Coq Standard Library</title> -</head> - -<body> - -<H1>The Coq Standard Library</H1> +<h1>The Coq Standard Library</h1> <p>Here is a short description of the Coq standard library, which is distributed with the system. @@ -210,7 +198,9 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Numbers</b>: An experimental modular architecture for arithmetic </dt> - <dt> <b> Prelude</b>: + <dd> + <dl> + <dt> <b> Prelude</b>:</dt> <dd> theories/Numbers/NumPrelude.v theories/Numbers/BigNumPrelude.v @@ -219,6 +209,7 @@ through the <tt>Require Import</tt> command.</p> <dt> <b> NatInt</b>: Abstract mixed natural/integer/cyclic arithmetic + </dt> <dd> theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -231,10 +222,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v </dd> - </dt> - <dt> <b> Cyclic</b>: + <dt> <b> Cyclic</b>: Abstract and 31-bits-based cyclic arithmetic + </dt> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -253,10 +244,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> - </dt> - <dt> <b> Natural</b>: + <dt> <b> Natural</b>: Abstract and 31-bits-words-based natural arithmetic + </dt> <dd> theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -279,10 +270,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v </dd> - </dt> <dt> <b> Integer</b>: Abstract and concrete (especially 31-bits-words-based) integer arithmetic + </dt> <dd> theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -303,17 +294,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v </dd> - </dt> <dt><b> Rational</b>: Abstract and 31-bits-words-based rational arithmetic + </dt> <dd> theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v </dd> - </dt> - </dt> + </dl> + </dd> <dt> <b>Relations</b>: Relations (definitions and basic results) @@ -353,7 +344,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Uniset.v </dd> - <dt> <b>Classes</b>: + <dt> <b>Classes</b>:</dt> <dd> theories/Classes/Init.v theories/Classes/RelationClasses.v @@ -368,7 +359,7 @@ through the <tt>Require Import</tt> command.</p> theories/Classes/RelationPairs.v </dd> - <dt> <b>Setoids</b>: + <dt> <b>Setoids</b>:</dt> <dd> theories/Setoids/Setoid.v </dd> @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coq.ml 13431 2010-09-18 08:15:29Z herbelin $ *) open Vernac open Vernacexpr @@ -479,7 +479,7 @@ let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc) let interp_last last = prerr_string "*"; try - vernac_com (States.with_heavy_rollback Vernacentries.interp) last; + vernac_com Vernacentries.interp last; Lib.add_frozen_state() with e -> let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); diff --git a/ide/preferences.ml b/ide/preferences.ml index 31d03ab9..5d97f659 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: preferences.ml 13436 2010-09-19 10:18:18Z herbelin $ *) open Configwin open Printf @@ -268,7 +268,12 @@ let load_pref () = set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v); set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v); set_hd "doc_url" (fun v -> - if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url then + if not (Flags.is_standard_doc_url v) && + v <> use_default_doc_url && + (* Extra hack to support links to last released doc version *) + v <> Coq_config.wwwcoq ^ "doc" && + v <> Coq_config.wwwcoq ^ "doc/" + then prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v); np.doc_url <- v); set_hd "library_url" (fun v -> np.library_url <- v); diff --git a/ide/uim/coqide-custom.scm b/ide/uim/coqide-custom.scm deleted file mode 100644 index 132bae7d..00000000 --- a/ide/uim/coqide-custom.scm +++ /dev/null @@ -1,105 +0,0 @@ -;;; coqide-custom.scm -- customization variables for coqide.scm -;;; -;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ -;;; -;;; All rights reserved. -;;; -;;; Redistribution and use in source and binary forms, with or without -;;; modification, are permitted provided that the following conditions -;;; are met: -;;; 1. Redistributions of source code must retain the above copyright -;;; notice, this list of conditions and the following disclaimer. -;;; 2. Redistributions in binary form must reproduce the above copyright -;;; notice, this list of conditions and the following disclaimer in the -;;; documentation and/or other materials provided with the distribution. -;;; 3. Neither the name of authors nor the names of its contributors -;;; may be used to endorse or promote products derived from this software -;;; without specific prior written permission. -;;; -;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND -;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE -;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT -;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY -;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF -;;; SUCH DAMAGE. -;;;; - -(require "i18n.scm") - -(define coqide-im-name-label (N_ "CoqIDE")) -(define coqide-im-short-desc (N_ "Emacs-style Latin characters input")) -(define coqide-im-long-desc (N_ "An input method for entering Latin letters used in European languages with the key translations adopted in Emacs.")) - -(define-custom-group 'coqide - coqide-im-name-label - coqide-im-short-desc) - -(define-custom-group 'coqide-properties - (N_ "Properties") - (N_ "long description will be here.")) - -(define-custom 'coqide-rules 'coqide-rules-latin-ltx - '(coqide coqide-properties) - (list 'choice - (list 'coqide-rules-british - (N_ "British") - (N_ "long description will be here.")) - (list 'coqide-rules-english-dvorak - (N_ "English Dvorak") - (N_ "long description will be here.")) - (list 'coqide-rules-latin-ltx - (N_ "LaTeX style") - (N_ "long description will be here."))) - (N_ "Latin characters keyboard layout") - (N_ "long description will be here.")) - -(custom-add-hook 'coqide-rules - 'custom-set-hooks - (lambda () - (map (lambda (lc) - (let ((new-rkc (rk-context-new - (symbol-value coqide-rules) #f #f))) - (coqide-context-flush lc) - (coqide-update-preedit lc) - (coqide-context-set-rkc! lc new-rkc))) - coqide-context-list))) - -;; For VI users. -(define-custom 'coqide-esc-turns-off? #f - '(coqide coqide-properties) - '(boolean) - (N_ "ESC turns off composition mode (for vi users)") - (N_ "long description will be here.")) - - -(define-custom-group 'coqide-keys - (N_ "CoqIDE key bindings") - (N_ "long description will be here.")) - -(define-custom 'coqide-on-key '("<Control>\\") - '(coqide coqide-keys) - '(key) - (N_ "CoqIDE on") - (N_ "long description will be here")) - -(define-custom 'coqide-off-key '("<Control>\\") - '(coqide coqide-keys) - '(key) - (N_ "CoqIDE off") - (N_ "long description will be here")) - -(define-custom 'coqide-backspace-key '(generic-backspace-key) - '(coqide coqide-keys) - '(key) - (N_ "CoqIDE backspace") - (N_ "long description will be here")) - -;; Local Variables: -;; mode: scheme -;; coding: utf-8 -;; End: diff --git a/ide/uim/coqide-rules.scm b/ide/uim/coqide-rules.scm deleted file mode 100644 index e41889c1..00000000 --- a/ide/uim/coqide-rules.scm +++ /dev/null @@ -1,1223 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; v ; The Coq Proof Assistant / The Coq Development Team ;; -;; <O___,, ; CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ;; -;; \VV/ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; // ; This file is distributed under the terms of the ;; -;; ; GNU Lesser General Public License Version 2.1 ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;; coqide-rules.scm -- key sequence tables for coqide.scm - -;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ -;; -;; All rights reserved. - -;; The translation tables in this file were derived from -;; the emacs-lisp source files latin-pre.el, latin-post.el, latin-alt.el -;; included in GNU Emacs. The following is the original copyright notice -;; therein, with the name GNU Emacs replaced by "this program". - -;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, -;; 2006, 2007 -;; Free Software Foundation, Inc. -;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, -;; 2006, 2007 -;; National Institute of Advanced Industrial Science and Technology (AIST) -;; Registration Number H14PRO021 - -;; This program is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation; either version 2, or (at your option) -;; any later version. - -;; This program is distributed in the hope that it will be useful, -;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -;; GNU General Public License for more details. - -;; You should have received a copy of the GNU General Public License -;; along with this program. If not, write to the -;; Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, -;; Boston, MA 02110-1301, USA. - -;;; Commentary: - -;; Key translation maps were originally copied from iso-acc.el. -;; latin-1-prefix: extra special characters added, adapted from the vim -;; digraphs (from J.H.M.Dassen <jdassen@wi.leidenuniv.nl>) -;; by R.F. Smith <rsmith@xs4all.nl> -;; -;; polish-slash: -;; Author: Włodek Bzyl <matwb@univ.gda.pl> -;; Maintainer: Włodek Bzyl <matwb@univ.gda.pl> -;; -;; latin-[89]-prefix: Dave Love <fx@gnu.org> - -(define coqide-rules-british '( -((("#")) ("£" "#")) -)) - -(define coqide-rules-english-dvorak '( -((("-")) ("[")) -((("=")) ("]")) -((("`")) ("`")) -((("q")) ("'")) -((("w")) (",")) -((("e")) (".")) -((("r")) ("p")) -((("t")) ("y")) -((("y")) ("f")) -((("u")) ("g")) -((("i")) ("c")) -((("o")) ("r")) -((("p")) ("l")) -((("[")) ("/")) -((("]")) ("=")) -((("a")) ("a")) -((("s")) ("o")) -((("d")) ("e")) -((("f")) ("u")) -((("g")) ("i")) -((("h")) ("d")) -((("j")) ("h")) -((("k")) ("t")) -((("l")) ("n")) -(((";")) ("s")) -((("'")) ("-")) -((("\\")) ("\\")) -((("z")) (";")) -((("x")) ("q")) -((("c")) ("j")) -((("v")) ("k")) -((("b")) ("x")) -((("n")) ("b")) -((("m")) ("m")) -(((",")) ("w")) -(((".")) ("v")) -((("/")) ("z")) -((("_")) ("{")) -((("+")) ("}")) -((("~")) ("~")) -((("Q")) ("\"")) -((("W")) ("<")) -((("E")) (">")) -((("R")) ("P")) -((("T")) ("Y")) -((("Y")) ("F")) -((("U")) ("G")) -((("I")) ("C")) -((("O")) ("R")) -((("P")) ("L")) -((("{")) ("?")) -((("}")) ("+")) -((("A")) ("A")) -((("S")) ("O")) -((("D")) ("E")) -((("F")) ("U")) -((("G")) ("I")) -((("H")) ("D")) -((("J")) ("H")) -((("K")) ("T")) -((("L")) ("N")) -(((":")) ("S")) -((("\"")) ("_")) -((("|")) ("|")) -((("Z")) (":")) -((("X")) ("Q")) -((("C")) ("J")) -((("V")) ("K")) -((("B")) ("X")) -((("N")) ("B")) -((("M")) ("M")) -((("<")) ("W")) -(((">")) ("V")) -((("?")) ("Z")) -)) - -(define coqide-rules-latin-ltx '( -((("!" "`")) ("¡")) -((("\\" "p" "o" "u" "n" "d" "s")) ("£")) -((("\\" "S")) ("§")) -((("\\" "\"" "{" "}")) ("¨")) -((("\\" "c" "o" "p" "y" "r" "i" "g" "h" "t")) ("©")) -((("$" "^" "a" "$")) ("ª")) -((("\\" "=" "{" "}")) ("¯")) -((("$" "\\" "p" "m" "$")) ("±")) -((("\\" "p" "m")) ("±")) -((("$" "^" "2" "$")) ("²")) -((("$" "^" "3" "$")) ("³")) -((("\\" "'" "{" "}")) ("´")) -((("\\" "P")) ("¶")) -((("$" "\\" "c" "d" "o" "t" "$")) ("·")) -((("\\" "c" "d" "o" "t")) ("·")) -((("\\" "c" "{" "}")) ("¸")) -((("$" "^" "1" "$")) ("¹")) -((("$" "^" "o" "$")) ("º")) -((("?" "`")) ("¿")) -((("\\" "`" "{" "A" "}")) ("À")) -((("\\" "`" "A")) ("À")) -((("\\" "'" "{" "A" "}")) ("Á")) -((("\\" "'" "A")) ("Á")) -((("\\" "^" "{" "A" "}")) ("Â")) -((("\\" "^" "A")) ("Â")) -((("\\" "~" "{" "A" "}")) ("Ã")) -((("\\" "~" "A")) ("Ã")) -((("\\" "\"" "{" "A" "}")) ("Ä")) -((("\\" "\"" "A")) ("Ä")) -((("\\" "k" "{" "A" "}")) ("Ą")) -((("\\" "A" "A")) ("Å")) -((("\\" "A" "E")) ("Æ")) -((("\\" "c" "{" "C" "}")) ("Ç")) -((("\\" "c" "C")) ("Ç")) -((("\\" "`" "{" "E" "}")) ("È")) -((("\\" "`" "E")) ("È")) -((("\\" "'" "{" "E" "}")) ("É")) -((("\\" "'" "E")) ("É")) -((("\\" "^" "{" "E" "}")) ("Ê")) -((("\\" "^" "E")) ("Ê")) -((("\\" "\"" "{" "E" "}")) ("Ë")) -((("\\" "\"" "E")) ("Ë")) -((("\\" "k" "{" "E" "}")) ("Ę")) -((("\\" "`" "{" "I" "}")) ("Ì")) -((("\\" "`" "I")) ("Ì")) -((("\\" "'" "{" "I" "}")) ("Í")) -((("\\" "'" "I")) ("Í")) -((("\\" "^" "{" "I" "}")) ("Î")) -((("\\" "^" "I")) ("Î")) -((("\\" "\"" "{" "I" "}")) ("Ï")) -((("\\" "\"" "I")) ("Ï")) -((("\\" "k" "{" "I" "}")) ("Į")) -((("\\" "~" "{" "N" "}")) ("Ñ")) -((("\\" "~" "N")) ("Ñ")) -((("\\" "`" "{" "O" "}")) ("Ò")) -((("\\" "`" "O")) ("Ò")) -((("\\" "'" "{" "O" "}")) ("Ó")) -((("\\" "'" "O")) ("Ó")) -((("\\" "^" "{" "O" "}")) ("Ô")) -((("\\" "^" "O")) ("Ô")) -((("\\" "~" "{" "O" "}")) ("Õ")) -((("\\" "~" "O")) ("Õ")) -((("\\" "\"" "{" "O" "}")) ("Ö")) -((("\\" "\"" "O")) ("Ö")) -((("\\" "k" "{" "O" "}")) ("Ǫ")) -((("$" "\\" "t" "i" "m" "e" "s" "$")) ("×")) -((("\\" "t" "i" "m" "e" "s")) ("×")) -((("\\" "O")) ("Ø")) -((("\\" "`" "{" "U" "}")) ("Ù")) -((("\\" "`" "U")) ("Ù")) -((("\\" "'" "{" "U" "}")) ("Ú")) -((("\\" "'" "U")) ("Ú")) -((("\\" "^" "{" "U" "}")) ("Û")) -((("\\" "^" "U")) ("Û")) -((("\\" "\"" "{" "U" "}")) ("Ü")) -((("\\" "\"" "U")) ("Ü")) -((("\\" "k" "{" "U" "}")) ("Ų")) -((("\\" "'" "{" "Y" "}")) ("Ý")) -((("\\" "'" "Y")) ("Ý")) -((("\\" "s" "s")) ("ß")) -((("\\" "`" "{" "a" "}")) ("à")) -((("\\" "`" "a")) ("à")) -((("\\" "'" "{" "a" "}")) ("á")) -((("\\" "'" "a")) ("á")) -((("\\" "^" "{" "a" "}")) ("â")) -((("\\" "^" "a")) ("â")) -((("\\" "~" "{" "a" "}")) ("ã")) -((("\\" "~" "a")) ("ã")) -((("\\" "\"" "{" "a" "}")) ("ä")) -((("\\" "\"" "a")) ("ä")) -((("\\" "k" "{" "a" "}")) ("ą")) -((("\\" "a" "a")) ("å")) -((("\\" "a" "e")) ("æ")) -((("\\" "c" "{" "c" "}")) ("ç")) -((("\\" "c" "c")) ("ç")) -((("\\" "`" "{" "e" "}")) ("è")) -((("\\" "`" "e")) ("è")) -((("\\" "'" "{" "e" "}")) ("é")) -((("\\" "'" "e")) ("é")) -((("\\" "^" "{" "e" "}")) ("ê")) -((("\\" "^" "e")) ("ê")) -((("\\" "\"" "{" "e" "}")) ("ë")) -((("\\" "\"" "e")) ("ë")) -((("\\" "k" "{" "e" "}")) ("ę")) -((("\\" "`" "{" "\\" "i" "}")) ("ì")) -((("\\" "`" "i")) ("ì")) -((("\\" "'" "{" "\\" "i" "}")) ("í")) -((("\\" "'" "i")) ("í")) -((("\\" "^" "{" "\\" "i" "}")) ("î")) -((("\\" "^" "i")) ("î")) -((("\\" "\"" "{" "\\" "i" "}")) ("ï")) -((("\\" "\"" "i")) ("ï")) -((("\\" "k" "{" "i" "}")) ("į")) -((("\\" "~" "{" "n" "}")) ("ñ")) -((("\\" "~" "n")) ("ñ")) -((("\\" "`" "{" "o" "}")) ("ò")) -((("\\" "`" "o")) ("ò")) -((("\\" "'" "{" "o" "}")) ("ó")) -((("\\" "'" "o")) ("ó")) -((("\\" "^" "{" "o" "}")) ("ô")) -((("\\" "^" "o")) ("ô")) -((("\\" "~" "{" "o" "}")) ("õ")) -((("\\" "~" "o")) ("õ")) -((("\\" "\"" "{" "o" "}")) ("ö")) -((("\\" "\"" "o")) ("ö")) -((("\\" "k" "{" "o" "}")) ("ǫ")) -((("$" "\\" "d" "i" "v" "$")) ("÷")) -((("\\" "d" "i" "v")) ("÷")) -((("\\" "o")) ("ø")) -((("\\" "`" "{" "u" "}")) ("ù")) -((("\\" "`" "u")) ("ù")) -((("\\" "'" "{" "u" "}")) ("ú")) -((("\\" "'" "u")) ("ú")) -((("\\" "^" "{" "u" "}")) ("û")) -((("\\" "^" "u")) ("û")) -((("\\" "\"" "{" "u" "}")) ("ü")) -((("\\" "\"" "u")) ("ü")) -((("\\" "k" "{" "u" "}")) ("ų")) -((("\\" "'" "{" "y" "}")) ("ý")) -((("\\" "'" "y")) ("ý")) -((("\\" "\"" "{" "y" "}")) ("ÿ")) -((("\\" "\"" "y")) ("ÿ")) -((("\\" "=" "{" "A" "}")) ("Ā")) -((("\\" "=" "A")) ("Ā")) -((("\\" "=" "{" "a" "}")) ("ā")) -((("\\" "=" "a")) ("ā")) -((("\\" "u" "{" "A" "}")) ("Ă")) -((("\\" "u" "A")) ("Ă")) -((("\\" "u" "{" "a" "}")) ("ă")) -((("\\" "u" "a")) ("ă")) -((("\\" "'" "{" "C" "}")) ("Ć")) -((("\\" "'" "C")) ("Ć")) -((("\\" "'" "{" "c" "}")) ("ć")) -((("\\" "'" "c")) ("ć")) -((("\\" "^" "{" "C" "}")) ("Ĉ")) -((("\\" "^" "C")) ("Ĉ")) -((("\\" "^" "{" "c" "}")) ("ĉ")) -((("\\" "^" "c")) ("ĉ")) -((("\\" "." "{" "C" "}")) ("Ċ")) -((("\\" "." "C")) ("Ċ")) -((("\\" "." "{" "c" "}")) ("ċ")) -((("\\" "." "c")) ("ċ")) -((("\\" "v" "{" "C" "}")) ("Č")) -((("\\" "v" "C")) ("Č")) -((("\\" "v" "{" "c" "}")) ("č")) -((("\\" "v" "c")) ("č")) -((("\\" "v" "{" "D" "}")) ("Ď")) -((("\\" "v" "D")) ("Ď")) -((("\\" "v" "{" "d" "}")) ("ď")) -((("\\" "v" "d")) ("ď")) -((("\\" "=" "{" "E" "}")) ("Ē")) -((("\\" "=" "E")) ("Ē")) -((("\\" "=" "{" "e" "}")) ("ē")) -((("\\" "=" "e")) ("ē")) -((("\\" "u" "{" "E" "}")) ("Ĕ")) -((("\\" "u" "E")) ("Ĕ")) -((("\\" "u" "{" "e" "}")) ("ĕ")) -((("\\" "u" "e")) ("ĕ")) -((("\\" "." "{" "E" "}")) ("Ė")) -((("\\" "." "E")) ("Ė")) -((("\\" "e" "{" "e" "}")) ("ė")) -((("\\" "e" "e")) ("ė")) -((("\\" "v" "{" "E" "}")) ("Ě")) -((("\\" "v" "E")) ("Ě")) -((("\\" "v" "{" "e" "}")) ("ě")) -((("\\" "v" "e")) ("ě")) -((("\\" "^" "{" "G" "}")) ("Ĝ")) -((("\\" "^" "G")) ("Ĝ")) -((("\\" "^" "{" "g" "}")) ("ĝ")) -((("\\" "^" "g")) ("ĝ")) -((("\\" "u" "{" "G" "}")) ("Ğ")) -((("\\" "u" "G")) ("Ğ")) -((("\\" "u" "{" "g" "}")) ("ğ")) -((("\\" "u" "g")) ("ğ")) -((("\\" "." "{" "G" "}")) ("Ġ")) -((("\\" "." "G")) ("Ġ")) -((("\\" "." "{" "g" "}")) ("ġ")) -((("\\" "." "g")) ("ġ")) -((("\\" "c" "{" "G" "}")) ("Ģ")) -((("\\" "c" "G")) ("Ģ")) -((("\\" "c" "{" "g" "}")) ("ģ")) -((("\\" "c" "g")) ("ģ")) -((("\\" "^" "{" "H" "}")) ("Ĥ")) -((("\\" "^" "H")) ("Ĥ")) -((("\\" "^" "{" "h" "}")) ("ĥ")) -((("\\" "^" "h")) ("ĥ")) -((("\\" "~" "{" "I" "}")) ("Ĩ")) -((("\\" "~" "I")) ("Ĩ")) -((("\\" "~" "{" "\\" "i" "}")) ("ĩ")) -((("\\" "~" "i")) ("ĩ")) -((("\\" "=" "{" "I" "}")) ("Ī")) -((("\\" "=" "I")) ("Ī")) -((("\\" "=" "{" "\\" "i" "}")) ("ī")) -((("\\" "=" "i")) ("ī")) -((("\\" "u" "{" "I" "}")) ("Ĭ")) -((("\\" "u" "I")) ("Ĭ")) -((("\\" "u" "{" "\\" "i" "}")) ("ĭ")) -((("\\" "u" "i")) ("ĭ")) -((("\\" "." "{" "I" "}")) ("İ")) -((("\\" "." "I")) ("İ")) -((("\\" "i")) ("ı")) -((("\\" "^" "{" "J" "}")) ("Ĵ")) -((("\\" "^" "J")) ("Ĵ")) -((("\\" "^" "{" "\\" "j" "}")) ("ĵ")) -((("\\" "^" "j")) ("ĵ")) -((("\\" "c" "{" "K" "}")) ("Ķ")) -((("\\" "c" "K")) ("Ķ")) -((("\\" "c" "{" "k" "}")) ("ķ")) -((("\\" "c" "k")) ("ķ")) -((("\\" "'" "{" "L" "}")) ("Ĺ")) -((("\\" "'" "L")) ("Ĺ")) -((("\\" "'" "{" "l" "}")) ("ĺ")) -((("\\" "'" "l")) ("ĺ")) -((("\\" "c" "{" "L" "}")) ("Ļ")) -((("\\" "c" "L")) ("Ļ")) -((("\\" "c" "{" "l" "}")) ("ļ")) -((("\\" "c" "l")) ("ļ")) -((("\\" "L")) ("Ł")) -((("\\" "l")) ("ł")) -((("\\" "'" "{" "N" "}")) ("Ń")) -((("\\" "'" "N")) ("Ń")) -((("\\" "'" "{" "n" "}")) ("ń")) -((("\\" "'" "n")) ("ń")) -((("\\" "c" "{" "N" "}")) ("Ņ")) -((("\\" "c" "N")) ("Ņ")) -((("\\" "c" "{" "n" "}")) ("ņ")) -((("\\" "c" "n")) ("ņ")) -((("\\" "v" "{" "N" "}")) ("Ň")) -((("\\" "v" "N")) ("Ň")) -((("\\" "v" "{" "n" "}")) ("ň")) -((("\\" "v" "n")) ("ň")) -((("\\" "=" "{" "O" "}")) ("Ō")) -((("\\" "=" "O")) ("Ō")) -((("\\" "=" "{" "o" "}")) ("ō")) -((("\\" "=" "o")) ("ō")) -((("\\" "u" "{" "O" "}")) ("Ŏ")) -((("\\" "u" "O")) ("Ŏ")) -((("\\" "u" "{" "o" "}")) ("ŏ")) -((("\\" "u" "o")) ("ŏ")) -((("\\" "H" "{" "O" "}")) ("Ő")) -((("\\" "H" "O")) ("Ő")) -((("\\" "U" "{" "o" "}")) ("ő")) -((("\\" "U" "o")) ("ő")) -((("\\" "O" "E")) ("Œ")) -((("\\" "o" "e")) ("œ")) -((("\\" "'" "{" "R" "}")) ("Ŕ")) -((("\\" "'" "R")) ("Ŕ")) -((("\\" "'" "{" "r" "}")) ("ŕ")) -((("\\" "'" "r")) ("ŕ")) -((("\\" "c" "{" "R" "}")) ("Ŗ")) -((("\\" "c" "R")) ("Ŗ")) -((("\\" "c" "{" "r" "}")) ("ŗ")) -((("\\" "c" "r")) ("ŗ")) -((("\\" "v" "{" "R" "}")) ("Ř")) -((("\\" "v" "R")) ("Ř")) -((("\\" "v" "{" "r" "}")) ("ř")) -((("\\" "v" "r")) ("ř")) -((("\\" "'" "{" "S" "}")) ("Ś")) -((("\\" "'" "S")) ("Ś")) -((("\\" "'" "{" "s" "}")) ("ś")) -((("\\" "'" "s")) ("ś")) -((("\\" "^" "{" "S" "}")) ("Ŝ")) -((("\\" "^" "S")) ("Ŝ")) -((("\\" "^" "{" "s" "}")) ("ŝ")) -((("\\" "^" "s")) ("ŝ")) -((("\\" "c" "{" "S" "}")) ("Ş")) -((("\\" "c" "S")) ("Ş")) -((("\\" "c" "{" "s" "}")) ("ş")) -((("\\" "c" "s")) ("ş")) -((("\\" "v" "{" "S" "}")) ("Š")) -((("\\" "v" "S")) ("Š")) -((("\\" "v" "{" "s" "}")) ("š")) -((("\\" "v" "s")) ("š")) -((("\\" "c" "{" "T" "}")) ("Ţ")) -((("\\" "c" "T")) ("Ţ")) -((("\\" "c" "{" "t" "}")) ("ţ")) -((("\\" "c" "t")) ("ţ")) -((("\\" "v" "{" "T" "}")) ("Ť")) -((("\\" "v" "T")) ("Ť")) -((("\\" "v" "{" "t" "}")) ("ť")) -((("\\" "v" "t")) ("ť")) -((("\\" "~" "{" "U" "}")) ("Ũ")) -((("\\" "~" "U")) ("Ũ")) -((("\\" "~" "{" "u" "}")) ("ũ")) -((("\\" "~" "u")) ("ũ")) -((("\\" "=" "{" "U" "}")) ("Ū")) -((("\\" "=" "U")) ("Ū")) -((("\\" "=" "{" "u" "}")) ("ū")) -((("\\" "=" "u")) ("ū")) -((("\\" "u" "{" "U" "}")) ("Ŭ")) -((("\\" "u" "U")) ("Ŭ")) -((("\\" "u" "{" "u" "}")) ("ŭ")) -((("\\" "u" "u")) ("ŭ")) -((("\\" "H" "{" "U" "}")) ("Ű")) -((("\\" "H" "U")) ("Ű")) -((("\\" "H" "{" "u" "}")) ("ű")) -((("\\" "H" "u")) ("ű")) -((("\\" "^" "{" "W" "}")) ("Ŵ")) -((("\\" "^" "W")) ("Ŵ")) -((("\\" "^" "{" "w" "}")) ("ŵ")) -((("\\" "^" "w")) ("ŵ")) -((("\\" "^" "{" "Y" "}")) ("Ŷ")) -((("\\" "^" "Y")) ("Ŷ")) -((("\\" "^" "{" "y" "}")) ("ŷ")) -((("\\" "^" "y")) ("ŷ")) -((("\\" "\"" "{" "Y" "}")) ("Ÿ")) -((("\\" "\"" "Y")) ("Ÿ")) -((("\\" "'" "{" "Z" "}")) ("Ź")) -((("\\" "'" "Z")) ("Ź")) -((("\\" "'" "{" "z" "}")) ("ź")) -((("\\" "'" "z")) ("ź")) -((("\\" "." "{" "Z" "}")) ("Ż")) -((("\\" "." "Z")) ("Ż")) -((("\\" "." "{" "z" "}")) ("ż")) -((("\\" "." "z")) ("ż")) -((("\\" "v" "{" "Z" "}")) ("Ž")) -((("\\" "v" "Z")) ("Ž")) -((("\\" "v" "{" "z" "}")) ("ž")) -((("\\" "v" "z")) ("ž")) -((("\\" "v" "{" "A" "}")) ("Ǎ")) -((("\\" "v" "A")) ("Ǎ")) -((("\\" "v" "{" "a" "}")) ("ǎ")) -((("\\" "v" "a")) ("ǎ")) -((("\\" "v" "{" "I" "}")) ("Ǐ")) -((("\\" "v" "I")) ("Ǐ")) -((("\\" "v" "{" "\\" "i" "}")) ("ǐ")) -((("\\" "v" "i")) ("ǐ")) -((("\\" "v" "{" "O" "}")) ("Ǒ")) -((("\\" "v" "O")) ("Ǒ")) -((("\\" "v" "{" "o" "}")) ("ǒ")) -((("\\" "v" "o")) ("ǒ")) -((("\\" "v" "{" "U" "}")) ("Ǔ")) -((("\\" "v" "U")) ("Ǔ")) -((("\\" "v" "{" "u" "}")) ("ǔ")) -((("\\" "v" "u")) ("ǔ")) -((("\\" "=" "{" "\\" "A" "E" "}")) ("Ǣ")) -((("\\" "=" "\\" "A" "E")) ("Ǣ")) -((("\\" "=" "{" "\\" "a" "e" "}")) ("ǣ")) -((("\\" "=" "\\" "a" "e")) ("ǣ")) -((("\\" "v" "{" "G" "}")) ("Ǧ")) -((("\\" "v" "G")) ("Ǧ")) -((("\\" "v" "{" "g" "}")) ("ǧ")) -((("\\" "v" "g")) ("ǧ")) -((("\\" "v" "{" "K" "}")) ("Ǩ")) -((("\\" "v" "K")) ("Ǩ")) -((("\\" "v" "{" "k" "}")) ("ǩ")) -((("\\" "v" "k")) ("ǩ")) -((("\\" "v" "{" "\\" "j" "}")) ("ǰ")) -((("\\" "v" "j")) ("ǰ")) -((("\\" "'" "{" "G" "}")) ("Ǵ")) -((("\\" "'" "G")) ("Ǵ")) -((("\\" "'" "{" "g" "}")) ("ǵ")) -((("\\" "'" "g")) ("ǵ")) -((("\\" "`" "{" "N" "}")) ("Ǹ")) -((("\\" "`" "N")) ("Ǹ")) -((("\\" "`" "{" "n" "}")) ("ǹ")) -((("\\" "`" "n")) ("ǹ")) -((("\\" "'" "{" "\\" "A" "E" "}")) ("Ǽ")) -((("\\" "'" "\\" "A" "E")) ("Ǽ")) -((("\\" "'" "{" "\\" "a" "e" "}")) ("ǽ")) -((("\\" "'" "\\" "a" "e")) ("ǽ")) -((("\\" "'" "{" "\\" "O" "}")) ("Ǿ")) -((("\\" "'" "\\" "O")) ("Ǿ")) -((("\\" "'" "{" "\\" "o" "}")) ("ǿ")) -((("\\" "'" "\\" "o")) ("ǿ")) -((("\\" "v" "{" "H" "}")) ("Ȟ")) -((("\\" "v" "H")) ("Ȟ")) -((("\\" "v" "{" "h" "}")) ("ȟ")) -((("\\" "v" "h")) ("ȟ")) -((("\\" "." "{" "A" "}")) ("Ȧ")) -((("\\" "." "A")) ("Ȧ")) -((("\\" "." "{" "a" "}")) ("ȧ")) -((("\\" "." "a")) ("ȧ")) -((("\\" "c" "{" "E" "}")) ("Ȩ")) -((("\\" "c" "E")) ("Ȩ")) -((("\\" "c" "{" "e" "}")) ("ȩ")) -((("\\" "c" "e")) ("ȩ")) -((("\\" "." "{" "O" "}")) ("Ȯ")) -((("\\" "." "O")) ("Ȯ")) -((("\\" "." "{" "o" "}")) ("ȯ")) -((("\\" "." "o")) ("ȯ")) -((("\\" "=" "{" "Y" "}")) ("Ȳ")) -((("\\" "=" "Y")) ("Ȳ")) -((("\\" "=" "{" "y" "}")) ("ȳ")) -((("\\" "=" "y")) ("ȳ")) -((("\\" "v" "{" "}")) ("ˇ")) -((("\\" "u" "{" "}")) ("˘")) -((("\\" "." "{" "}")) ("˙")) -((("\\" "~" "{" "}")) ("˜")) -((("\\" "H" "{" "}")) ("˝")) -((("\\" "'")) ("́")) -((("\\" "'" "K")) ("Ḱ")) -((("\\" "'" "M")) ("Ḿ")) -((("\\" "'" "P")) ("Ṕ")) -((("\\" "'" "W")) ("Ẃ")) -((("\\" "'" "k")) ("ḱ")) -((("\\" "'" "m")) ("ḿ")) -((("\\" "'" "p")) ("ṕ")) -((("\\" "'" "w")) ("ẃ")) -((("\\" ",")) (" ")) -((("\\" ".")) ("̇")) -((("\\" "." "B")) ("Ḃ")) -((("\\" "." "D")) ("Ḋ")) -((("\\" "." "F")) ("Ḟ")) -((("\\" "." "H")) ("Ḣ")) -((("\\" "." "M")) ("Ṁ")) -((("\\" "." "N")) ("Ṅ")) -((("\\" "." "P")) ("Ṗ")) -((("\\" "." "R")) ("Ṙ")) -((("\\" "." "S")) ("Ṡ")) -((("\\" "." "T")) ("Ṫ")) -((("\\" "." "W")) ("Ẇ")) -((("\\" "." "X")) ("Ẋ")) -((("\\" "." "Y")) ("Ẏ")) -((("\\" "." "b")) ("ḃ")) -((("\\" "." "d")) ("ḋ")) -((("\\" "." "e")) ("ė")) -((("\\" "." "f")) ("ḟ")) -((("\\" "." "h")) ("ḣ")) -((("\\" "." "m")) ("ṁ")) -((("\\" "." "n")) ("ṅ")) -((("\\" "." "p")) ("ṗ")) -((("\\" "." "r")) ("ṙ")) -((("\\" "." "s")) ("ṡ")) -((("\\" "." "t")) ("ṫ")) -((("\\" "." "w")) ("ẇ")) -((("\\" "." "x")) ("ẋ")) -((("\\" "." "y")) ("ẏ")) -((("\\" "/")) ("")) -((("\\" ":")) (" ")) -((("\\" ";")) (" ")) -((("\\" "=")) ("̄")) -((("\\" "=" "G")) ("Ḡ")) -((("\\" "=" "g")) ("ḡ")) -((("^" "(")) ("⁽")) -((("^" ")")) ("⁾")) -((("^" "+")) ("⁺")) -((("^" "-")) ("⁻")) -((("^" "0")) ("⁰")) -((("^" "1")) ("¹")) -((("^" "2")) ("²")) -((("^" "3")) ("³")) -((("^" "4")) ("⁴")) -((("^" "5")) ("⁵")) -((("^" "6")) ("⁶")) -((("^" "7")) ("⁷")) -((("^" "8")) ("⁸")) -((("^" "9")) ("⁹")) -((("^" "=")) ("⁼")) -((("^" "\\" "g" "a" "m" "m" "a")) ("ˠ")) -((("^" "h")) ("ʰ")) -((("^" "j")) ("ʲ")) -((("^" "l")) ("ˡ")) -((("^" "n")) ("ⁿ")) -((("^" "o")) ("º")) -((("^" "r")) ("ʳ")) -((("^" "s")) ("ˢ")) -((("^" "w")) ("ʷ")) -((("^" "x")) ("ˣ")) -((("^" "y")) ("ʸ")) -((("^" "{" "S" "M" "}")) ("℠")) -((("^" "{" "T" "E" "L" "}")) ("℡")) -((("^" "{" "T" "M" "}")) ("™")) -((("_" "(")) ("₍")) -((("_" ")")) ("₎")) -((("_" "+")) ("₊")) -((("_" "-")) ("₋")) -((("_" "0")) ("₀")) -((("_" "1")) ("₁")) -((("_" "2")) ("₂")) -((("_" "3")) ("₃")) -((("_" "4")) ("₄")) -((("_" "5")) ("₅")) -((("_" "6")) ("₆")) -((("_" "7")) ("₇")) -((("_" "8")) ("₈")) -((("_" "9")) ("₉")) -((("_" "=")) ("₌")) -((("\\" "~")) ("̃")) -((("\\" "~" "E")) ("Ẽ")) -((("\\" "~" "V")) ("Ṽ")) -((("\\" "~" "Y")) ("Ỹ")) -((("\\" "~" "e")) ("ẽ")) -((("\\" "~" "v")) ("ṽ")) -((("\\" "~" "y")) ("ỹ")) -((("\\" "\"")) ("̈")) -((("\\" "\"" "H")) ("Ḧ")) -((("\\" "\"" "W")) ("Ẅ")) -((("\\" "\"" "X")) ("Ẍ")) -((("\\" "\"" "h")) ("ḧ")) -((("\\" "\"" "t")) ("ẗ")) -((("\\" "\"" "w")) ("ẅ")) -((("\\" "\"" "x")) ("ẍ")) -((("\\" "^")) ("̂")) -((("\\" "^" "Z")) ("Ẑ")) -((("\\" "^" "z")) ("ẑ")) -((("\\" "`")) ("̀")) -((("\\" "`" "W")) ("Ẁ")) -((("\\" "`" "Y")) ("Ỳ")) -((("\\" "`" "w")) ("ẁ")) -((("\\" "`" "y")) ("ỳ")) -((("\\" "b")) ("̱")) -((("\\" "c")) ("̧")) -((("\\" "c" "{" "D" "}")) ("Ḑ")) -((("\\" "c" "{" "H" "}")) ("Ḩ")) -((("\\" "c" "{" "d" "}")) ("ḑ")) -((("\\" "c" "{" "h" "}")) ("ḩ")) -((("\\" "d")) ("̣")) -((("\\" "d" "{" "A" "}")) ("Ạ")) -((("\\" "d" "{" "B" "}")) ("Ḅ")) -((("\\" "d" "{" "D" "}")) ("Ḍ")) -((("\\" "d" "{" "E" "}")) ("Ẹ")) -((("\\" "d" "{" "H" "}")) ("Ḥ")) -((("\\" "d" "{" "I" "}")) ("Ị")) -((("\\" "d" "{" "K" "}")) ("Ḳ")) -((("\\" "d" "{" "L" "}")) ("Ḷ")) -((("\\" "d" "{" "M" "}")) ("Ṃ")) -((("\\" "d" "{" "N" "}")) ("Ṇ")) -((("\\" "d" "{" "O" "}")) ("Ọ")) -((("\\" "d" "{" "R" "}")) ("Ṛ")) -((("\\" "d" "{" "S" "}")) ("Ṣ")) -((("\\" "d" "{" "T" "}")) ("Ṭ")) -((("\\" "d" "{" "U" "}")) ("Ụ")) -((("\\" "d" "{" "V" "}")) ("Ṿ")) -((("\\" "d" "{" "W" "}")) ("Ẉ")) -((("\\" "d" "{" "Y" "}")) ("Ỵ")) -((("\\" "d" "{" "Z" "}")) ("Ẓ")) -((("\\" "d" "{" "a" "}")) ("ạ")) -((("\\" "d" "{" "b" "}")) ("ḅ")) -((("\\" "d" "{" "d" "}")) ("ḍ")) -((("\\" "d" "{" "e" "}")) ("ẹ")) -((("\\" "d" "{" "h" "}")) ("ḥ")) -((("\\" "d" "{" "i" "}")) ("ị")) -((("\\" "d" "{" "k" "}")) ("ḳ")) -((("\\" "d" "{" "l" "}")) ("ḷ")) -((("\\" "d" "{" "m" "}")) ("ṃ")) -((("\\" "d" "{" "n" "}")) ("ṇ")) -((("\\" "d" "{" "o" "}")) ("ọ")) -((("\\" "d" "{" "r" "}")) ("ṛ")) -((("\\" "d" "{" "s" "}")) ("ṣ")) -((("\\" "d" "{" "t" "}")) ("ṭ")) -((("\\" "d" "{" "u" "}")) ("ụ")) -((("\\" "d" "{" "v" "}")) ("ṿ")) -((("\\" "d" "{" "w" "}")) ("ẉ")) -((("\\" "d" "{" "y" "}")) ("ỵ")) -((("\\" "d" "{" "z" "}")) ("ẓ")) -((("\\" "r" "q")) ("’")) -((("\\" "u")) ("̆")) -((("\\" "v")) ("̌")) -((("\\" "v" "{" "L" "}")) ("Ľ")) -((("\\" "v" "{" "i" "}")) ("ǐ")) -((("\\" "v" "{" "j" "}")) ("ǰ")) -((("\\" "v" "{" "l" "}")) ("ľ")) -((("\\" "y" "e" "n")) ("¥")) -((("\\" "B" "o" "x")) ("□")) -((("\\" "B" "u" "m" "p" "e" "q")) ("≎")) -((("\\" "C" "a" "p")) ("⋒")) -((("\\" "C" "u" "p")) ("⋓")) -((("\\" "D" "e" "l" "t" "a")) ("Δ")) -((("\\" "D" "i" "a" "m" "o" "n" "d")) ("◇")) -((("\\" "D" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇓")) -((("\\" "G" "a" "m" "m" "a")) ("Γ")) -((("\\" "H")) ("̋")) -((("\\" "H" "{" "o" "}")) ("ő")) -((("\\" "I" "m")) ("ℑ")) -((("\\" "J" "o" "i" "n")) ("⋈")) -((("\\" "L" "a" "m" "b" "d" "a")) ("Λ")) -((("\\" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐")) -((("\\" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔")) -((("\\" "L" "l")) ("⋘")) -((("\\" "L" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇚")) -((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐")) -((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔")) -((("\\" "L" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒")) -((("\\" "L" "s" "h")) ("↰")) -((("\\" "O" "m" "e" "g" "a")) ("Ω")) -((("\\" "P" "h" "i")) ("Φ")) -((("\\" "P" "i")) ("Π")) -((("\\" "P" "s" "i")) ("Ψ")) -((("\\" "R" "e")) ("ℜ")) -((("\\" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒")) -((("\\" "R" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇛")) -((("\\" "R" "s" "h")) ("↱")) -((("\\" "S" "i" "g" "m" "a")) ("Σ")) -((("\\" "S" "u" "b" "s" "e" "t")) ("⋐")) -((("\\" "S" "u" "p" "s" "e" "t")) ("⋑")) -((("\\" "T" "h" "e" "t" "a")) ("Θ")) -((("\\" "U" "p" "a" "r" "r" "o" "w")) ("⇑")) -((("\\" "U" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇕")) -((("\\" "U" "p" "s" "i" "l" "o" "n")) ("Υ")) -((("\\" "V" "d" "a" "s" "h")) ("⊩")) -((("\\" "V" "e" "r" "t")) ("‖")) -((("\\" "V" "v" "d" "a" "s" "h")) ("⊪")) -((("\\" "X" "i")) ("Ξ")) -((("\\" "a" "l" "e" "p" "h")) ("א")) -((("\\" "a" "l" "p" "h" "a")) ("α")) -((("\\" "a" "m" "a" "l" "g")) ("∐")) -((("\\" "a" "n" "g" "l" "e")) ("∠")) -((("\\" "a" "p" "p" "r" "o" "x")) ("≈")) -((("\\" "a" "p" "p" "r" "o" "x" "e" "q")) ("≊")) -((("\\" "a" "s" "t")) ("∗")) -((("\\" "a" "s" "y" "m" "p")) ("≍")) -((("\\" "b" "a" "c" "k" "c" "o" "n" "g")) ("≌")) -((("\\" "b" "a" "c" "k" "e" "p" "s" "i" "l" "o" "n")) ("∍")) -((("\\" "b" "a" "c" "k" "p" "r" "i" "m" "e")) ("‵")) -((("\\" "b" "a" "c" "k" "s" "i" "m")) ("∽")) -((("\\" "b" "a" "c" "k" "s" "i" "m" "e" "q")) ("⋍")) -((("\\" "b" "a" "c" "k" "s" "l" "a" "s" "h")) ("\\")) -((("\\" "b" "a" "r" "w" "e" "d" "g" "e")) ("⊼")) -((("\\" "b" "e" "c" "a" "u" "s" "e")) ("∵")) -((("\\" "b" "e" "t" "a")) ("β")) -((("\\" "b" "e" "t" "h")) ("ב")) -((("\\" "b" "e" "t" "w" "e" "e" "n")) ("≬")) -((("\\" "b" "i" "g" "c" "a" "p")) ("⋂")) -((("\\" "b" "i" "g" "c" "i" "r" "c")) ("◯")) -((("\\" "b" "i" "g" "c" "u" "p")) ("⋃")) -((("\\" "b" "i" "g" "s" "t" "a" "r")) ("★")) -((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▽")) -((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "u" "p")) ("△")) -((("\\" "b" "i" "g" "v" "e" "e")) ("⋁")) -((("\\" "b" "i" "g" "w" "e" "d" "g" "e")) ("⋀")) -((("\\" "b" "l" "a" "c" "k" "l" "o" "z" "e" "n" "g" "e")) ("✦")) -((("\\" "b" "l" "a" "c" "k" "s" "q" "u" "a" "r" "e")) ("▪")) -((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e")) ("▴")) -((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▾")) -((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◂")) -((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▸")) -((("\\" "b" "o" "t")) ("⊥")) -((("\\" "b" "o" "w" "t" "i" "e")) ("⋈")) -((("\\" "b" "o" "x" "m" "i" "n" "u" "s")) ("⊟")) -((("\\" "b" "o" "x" "p" "l" "u" "s")) ("⊞")) -((("\\" "b" "o" "x" "t" "i" "m" "e" "s")) ("⊠")) -((("\\" "b" "u" "l" "l" "e" "t")) ("•")) -((("\\" "b" "u" "m" "p" "e" "q")) ("≏")) -((("\\" "c" "a" "p")) ("∩")) -((("\\" "c" "d" "o" "t" "s")) ("⋯")) -((("\\" "c" "e" "n" "t" "e" "r" "d" "o" "t")) ("·")) -((("\\" "c" "h" "e" "c" "k" "m" "a" "r" "k")) ("✓")) -((("\\" "c" "h" "i")) ("χ")) -((("\\" "c" "i" "r" "c")) ("○")) -((("\\" "c" "i" "r" "c" "e" "q")) ("≗")) -((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↺")) -((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↻")) -((("\\" "c" "i" "r" "c" "l" "e" "d" "R")) ("®")) -((("\\" "c" "i" "r" "c" "l" "e" "d" "S")) ("Ⓢ")) -((("\\" "c" "i" "r" "c" "l" "e" "d" "a" "s" "t")) ("⊛")) -((("\\" "c" "i" "r" "c" "l" "e" "d" "c" "i" "r" "c")) ("⊚")) -((("\\" "c" "i" "r" "c" "l" "e" "d" "d" "a" "s" "h")) ("⊝")) -((("\\" "c" "l" "u" "b" "s" "u" "i" "t")) ("♣")) -((("\\" "c" "o" "l" "o" "n")) (":")) -((("\\" "c" "o" "l" "o" "n" "e" "q")) ("≔")) -((("\\" "c" "o" "m" "p" "l" "e" "m" "e" "n" "t")) ("∁")) -((("\\" "c" "o" "n" "g")) ("≅")) -((("\\" "c" "o" "p" "r" "o" "d")) ("∐")) -((("\\" "c" "u" "p")) ("∪")) -((("\\" "c" "u" "r" "l" "y" "e" "q" "p" "r" "e" "c")) ("⋞")) -((("\\" "c" "u" "r" "l" "y" "e" "q" "s" "u" "c" "c")) ("⋟")) -((("\\" "c" "u" "r" "l" "y" "p" "r" "e" "c" "e" "q")) ("≼")) -((("\\" "c" "u" "r" "l" "y" "v" "e" "e")) ("⋎")) -((("\\" "c" "u" "r" "l" "y" "w" "e" "d" "g" "e")) ("⋏")) -((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↶")) -((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↷")) -((("\\" "d" "a" "g")) ("†")) -((("\\" "d" "a" "g" "g" "e" "r")) ("†")) -((("\\" "d" "a" "l" "e" "t" "h")) ("ד")) -((("\\" "d" "a" "s" "h" "v")) ("⊣")) -((("\\" "d" "d" "a" "g")) ("‡")) -((("\\" "d" "d" "a" "g" "g" "e" "r")) ("‡")) -((("\\" "d" "d" "o" "t" "s")) ("⋱")) -((("\\" "d" "e" "l" "t" "a")) ("δ")) -((("\\" "d" "i" "a" "m" "o" "n" "d")) ("⋄")) -((("\\" "d" "i" "a" "m" "o" "n" "d" "s" "u" "i" "t")) ("♢")) -((("\\" "d" "i" "g" "a" "m" "m" "a")) ("Ϝ")) -((("\\" "d" "i" "v" "i" "d" "e" "o" "n" "t" "i" "m" "e" "s")) ("⋇")) -((("\\" "d" "o" "t" "e" "q")) ("≐")) -((("\\" "d" "o" "t" "e" "q" "d" "o" "t")) ("≑")) -((("\\" "d" "o" "t" "p" "l" "u" "s")) ("∔")) -((("\\" "d" "o" "t" "s" "q" "u" "a" "r" "e")) ("⊡")) -((("\\" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↓")) -((("\\" "d" "o" "w" "n" "d" "o" "w" "n" "a" "r" "r" "o" "w" "s")) ("⇊")) -((("\\" "d" "o" "w" "n" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇃")) -((("\\" "d" "o" "w" "n" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇂")) -((("\\" "e" "l" "l")) ("ℓ")) -((("\\" "e" "m" "p" "t" "y" "s" "e" "t")) ("∅")) -((("\\" "e" "p" "s" "i" "l" "o" "n")) ("ε")) -((("\\" "e" "q" "c" "i" "r" "c")) ("≖")) -((("\\" "e" "q" "c" "o" "l" "o" "n")) ("≕")) -((("\\" "e" "q" "s" "l" "a" "n" "t" "g" "t" "r")) ("⋝")) -((("\\" "e" "q" "s" "l" "a" "n" "t" "l" "e" "s" "s")) ("⋜")) -((("\\" "e" "q" "u" "i" "v")) ("≡")) -((("\\" "e" "t" "a")) ("η")) -((("\\" "e" "u" "r" "o")) ("€")) -((("\\" "e" "x" "i" "s" "t" "s")) ("∃")) -((("\\" "f" "a" "l" "l" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≒")) -((("\\" "f" "l" "a" "t")) ("♭")) -((("\\" "f" "o" "r" "a" "l" "l")) ("∀")) -((("\\" "f" "r" "a" "c" "1")) ("⅟")) -((("\\" "f" "r" "a" "c" "1" "2")) ("½")) -((("\\" "f" "r" "a" "c" "1" "3")) ("⅓")) -((("\\" "f" "r" "a" "c" "1" "4")) ("¼")) -((("\\" "f" "r" "a" "c" "1" "5")) ("⅕")) -((("\\" "f" "r" "a" "c" "1" "6")) ("⅙")) -((("\\" "f" "r" "a" "c" "1" "8")) ("⅛")) -((("\\" "f" "r" "a" "c" "2" "3")) ("⅔")) -((("\\" "f" "r" "a" "c" "2" "5")) ("⅖")) -((("\\" "f" "r" "a" "c" "3" "4")) ("¾")) -((("\\" "f" "r" "a" "c" "3" "5")) ("⅗")) -((("\\" "f" "r" "a" "c" "3" "8")) ("⅜")) -((("\\" "f" "r" "a" "c" "4" "5")) ("⅘")) -((("\\" "f" "r" "a" "c" "5" "6")) ("⅚")) -((("\\" "f" "r" "a" "c" "5" "8")) ("⅝")) -((("\\" "f" "r" "a" "c" "7" "8")) ("⅞")) -((("\\" "f" "r" "o" "w" "n")) ("⌢")) -((("\\" "g" "a" "m" "m" "a")) ("γ")) -((("\\" "g" "e")) ("≥")) -((("\\" "g" "e" "q")) ("≥")) -((("\\" "g" "e" "q" "q")) ("≧")) -((("\\" "g" "e" "q" "s" "l" "a" "n" "t")) ("≥")) -((("\\" "g" "e" "t" "s")) ("←")) -((("\\" "g" "g")) ("≫")) -((("\\" "g" "g" "g")) ("⋙")) -((("\\" "g" "i" "m" "e" "l")) ("ג")) -((("\\" "g" "n" "a" "p" "p" "r" "o" "x")) ("⋧")) -((("\\" "g" "n" "e" "q")) ("≩")) -((("\\" "g" "n" "e" "q" "q")) ("≩")) -((("\\" "g" "n" "s" "i" "m")) ("⋧")) -((("\\" "g" "t" "r" "a" "p" "p" "r" "o" "x")) ("≳")) -((("\\" "g" "t" "r" "d" "o" "t")) ("⋗")) -((("\\" "g" "t" "r" "e" "q" "l" "e" "s" "s")) ("⋛")) -((("\\" "g" "t" "r" "e" "q" "q" "l" "e" "s" "s")) ("⋛")) -((("\\" "g" "t" "r" "l" "e" "s" "s")) ("≷")) -((("\\" "g" "t" "r" "s" "i" "m")) ("≳")) -((("\\" "g" "v" "e" "r" "t" "n" "e" "q" "q")) ("≩")) -((("\\" "h" "b" "a" "r")) ("ℏ")) -((("\\" "h" "e" "a" "r" "t" "s" "u" "i" "t")) ("♥")) -((("\\" "h" "o" "o" "k" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↩")) -((("\\" "h" "o" "o" "k" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↪")) -((("\\" "i" "f" "f")) ("⇔")) -((("\\" "i" "m" "a" "t" "h")) ("ı")) -((("\\" "i" "n")) ("∈")) -((("\\" "i" "n" "f" "t" "y")) ("∞")) -((("\\" "i" "n" "t")) ("∫")) -((("\\" "i" "n" "t" "e" "r" "c" "a" "l")) ("⊺")) -((("\\" "i" "o" "t" "a")) ("ι")) -((("\\" "k" "a" "p" "p" "a")) ("κ")) -((("\\" "l" "a" "m" "b" "d" "a")) ("λ")) -((("\\" "l" "a" "n" "g" "l" "e")) ("〈")) -((("\\" "l" "b" "r" "a" "c" "e")) ("{")) -((("\\" "l" "b" "r" "a" "c" "k")) ("[")) -((("\\" "l" "c" "e" "i" "l")) ("⌈")) -((("\\" "l" "d" "o" "t" "s")) ("…")) -((("\\" "l" "e")) ("≤")) -((("\\" "l" "e" "a" "d" "s" "t" "o")) ("↝")) -((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←")) -((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↢")) -((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("↽")) -((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("↼")) -((("\\" "l" "e" "f" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇇")) -((("\\" "l" "e" "f" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〈")) -((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔")) -((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇆")) -((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇋")) -((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w")) ("↭")) -((("\\" "l" "e" "f" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋋")) -((("\\" "l" "e" "q")) ("≤")) -((("\\" "l" "e" "q" "q")) ("≦")) -((("\\" "l" "e" "q" "s" "l" "a" "n" "t")) ("≤")) -((("\\" "l" "e" "s" "s" "a" "p" "p" "r" "o" "x")) ("≲")) -((("\\" "l" "e" "s" "s" "d" "o" "t")) ("⋖")) -((("\\" "l" "e" "s" "s" "e" "q" "g" "t" "r")) ("⋚")) -((("\\" "l" "e" "s" "s" "e" "q" "q" "g" "t" "r")) ("⋚")) -((("\\" "l" "e" "s" "s" "g" "t" "r")) ("≶")) -((("\\" "l" "e" "s" "s" "s" "i" "m")) ("≲")) -((("\\" "l" "f" "l" "o" "o" "r")) ("⌊")) -((("\\" "l" "h" "d")) ("◁")) -((("\\" "r" "h" "d")) ("▷")) -((("\\" "l" "l")) ("≪")) -((("\\" "l" "l" "c" "o" "r" "n" "e" "r")) ("⌞")) -((("\\" "l" "n" "a" "p" "p" "r" "o" "x")) ("⋦")) -((("\\" "l" "n" "e" "q")) ("≨")) -((("\\" "l" "n" "e" "q" "q")) ("≨")) -((("\\" "l" "n" "s" "i" "m")) ("⋦")) -((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←")) -((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔")) -((("\\" "l" "o" "n" "g" "m" "a" "p" "s" "t" "o")) ("↦")) -((("\\" "l" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→")) -((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↫")) -((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↬")) -((("\\" "l" "o" "z" "e" "n" "g" "e")) ("✧")) -((("\\" "l" "q")) ("‘")) -((("\\" "l" "r" "c" "o" "r" "n" "e" "r")) ("⌟")) -((("\\" "l" "t" "i" "m" "e" "s")) ("⋉")) -((("\\" "l" "v" "e" "r" "t" "n" "e" "q" "q")) ("≨")) -((("\\" "m" "a" "l" "t" "e" "s" "e")) ("✠")) -((("\\" "m" "a" "p" "s" "t" "o")) ("↦")) -((("\\" "m" "e" "a" "s" "u" "r" "e" "d" "a" "n" "g" "l" "e")) ("∡")) -((("\\" "m" "h" "o")) ("℧")) -((("\\" "m" "i" "d")) ("∣")) -((("\\" "m" "o" "d" "e" "l" "s")) ("⊧")) -((("\\" "m" "p")) ("∓")) -((("\\" "m" "u" "l" "t" "i" "m" "a" "p")) ("⊸")) -((("\\" "n" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇍")) -((("\\" "n" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇎")) -((("\\" "n" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇏")) -((("\\" "n" "V" "D" "a" "s" "h")) ("⊯")) -((("\\" "n" "V" "d" "a" "s" "h")) ("⊮")) -((("\\" "n" "a" "b" "l" "a")) ("∇")) -((("\\" "n" "a" "p" "p" "r" "o" "x")) ("≉")) -((("\\" "n" "a" "t" "u" "r" "a" "l")) ("♮")) -((("\\" "n" "c" "o" "n" "g")) ("≇")) -((("\\" "n" "e")) ("≠")) -((("\\" "n" "e" "a" "r" "r" "o" "w")) ("↗")) -((("\\" "n" "e" "g")) ("¬")) -((("\\" "n" "e" "q")) ("≠")) -((("\\" "n" "e" "q" "u" "i" "v")) ("≢")) -((("\\" "n" "e" "w" "l" "i" "n" "e")) ("
")) -((("\\" "n" "e" "x" "i" "s" "t" "s")) ("∄")) -((("\\" "n" "g" "e" "q")) ("≱")) -((("\\" "n" "g" "e" "q" "q")) ("≱")) -((("\\" "n" "g" "e" "q" "s" "l" "a" "n" "t")) ("≱")) -((("\\" "n" "g" "t" "r")) ("≯")) -((("\\" "n" "i")) ("∋")) -((("\\" "n" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↚")) -((("\\" "n" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↮")) -((("\\" "n" "l" "e" "q")) ("≰")) -((("\\" "n" "l" "e" "q" "q")) ("≰")) -((("\\" "n" "l" "e" "q" "s" "l" "a" "n" "t")) ("≰")) -((("\\" "n" "l" "e" "s" "s")) ("≮")) -((("\\" "n" "m" "i" "d")) ("∤")) -((("\\" "n" "o" "t")) ("̸")) -((("\\" "n" "o" "t" "i" "n")) ("∉")) -((("\\" "n" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦")) -((("\\" "n" "p" "r" "e" "c")) ("⊀")) -((("\\" "n" "p" "r" "e" "c" "e" "q")) ("⋠")) -((("\\" "n" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↛")) -((("\\" "n" "s" "h" "o" "r" "t" "m" "i" "d")) ("∤")) -((("\\" "n" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦")) -((("\\" "n" "s" "i" "m")) ("≁")) -((("\\" "n" "s" "i" "m" "e" "q")) ("≄")) -((("\\" "n" "s" "u" "b" "s" "e" "t")) ("⊄")) -((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊈")) -((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊈")) -((("\\" "n" "s" "u" "c" "c")) ("⊁")) -((("\\" "n" "s" "u" "c" "c" "e" "q")) ("⋡")) -((("\\" "n" "s" "u" "p" "s" "e" "t")) ("⊅")) -((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊉")) -((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊉")) -((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⋪")) -((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⋬")) -((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⋫")) -((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⋭")) -((("\\" "n" "u")) ("ν")) -((("\\" "n" "v" "D" "a" "s" "h")) ("⊭")) -((("\\" "n" "v" "d" "a" "s" "h")) ("⊬")) -((("\\" "n" "w" "a" "r" "r" "o" "w")) ("↖")) -((("\\" "o" "d" "o" "t")) ("⊙")) -((("\\" "o" "i" "n" "t")) ("∮")) -((("\\" "o" "m" "e" "g" "a")) ("ω")) -((("\\" "o" "m" "i" "n" "u" "s")) ("⊖")) -((("\\" "o" "p" "l" "u" "s")) ("⊕")) -((("\\" "o" "s" "l" "a" "s" "h")) ("⊘")) -((("\\" "o" "t" "i" "m" "e" "s")) ("⊗")) -((("\\" "p" "a" "r")) ("
")) -((("\\" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥")) -((("\\" "p" "a" "r" "t" "i" "a" "l")) ("∂")) -((("\\" "p" "e" "r" "p")) ("⊥")) -((("\\" "p" "h" "i")) ("φ")) -((("\\" "p" "i")) ("π")) -((("\\" "p" "i" "t" "c" "h" "f" "o" "r" "k")) ("⋔")) -((("\\" "p" "r" "e" "c")) ("≺")) -((("\\" "p" "r" "e" "c" "a" "p" "p" "r" "o" "x")) ("≾")) -((("\\" "p" "r" "e" "c" "e" "q")) ("≼")) -((("\\" "p" "r" "e" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋨")) -((("\\" "p" "r" "e" "c" "n" "s" "i" "m")) ("⋨")) -((("\\" "p" "r" "e" "c" "s" "i" "m")) ("≾")) -((("\\" "p" "r" "i" "m" "e")) ("′")) -((("\\" "p" "r" "o" "d")) ("∏")) -((("\\" "p" "r" "o" "p" "t" "o")) ("∝")) -((("\\" "p" "s" "i")) ("ψ")) -((("\\" "q" "e" "d")) ("∎")) -((("\\" "q" "u" "a" "d")) (" ")) -((("\\" "r" "a" "n" "g" "l" "e")) ("〉")) -((("\\" "r" "b" "r" "a" "c" "e")) ("}")) -((("\\" "r" "b" "r" "a" "c" "k")) ("]")) -((("\\" "r" "c" "e" "i" "l")) ("⌉")) -((("\\" "r" "f" "l" "o" "o" "r")) ("⌋")) -((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→")) -((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↣")) -((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("⇁")) -((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("⇀")) -((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇄")) -((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇌")) -((("\\" "r" "i" "g" "h" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〉")) -((("\\" "r" "i" "g" "h" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇉")) -((("\\" "r" "i" "g" "h" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋌")) -((("\\" "r" "i" "s" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≓")) -((("\\" "r" "t" "i" "m" "e" "s")) ("⋊")) -((("\\" "s" "b" "s")) ("﹨")) -((("\\" "s" "e" "a" "r" "r" "o" "w")) ("↘")) -((("\\" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖")) -((("\\" "s" "h" "a" "r" "p")) ("♯")) -((("\\" "s" "h" "o" "r" "t" "m" "i" "d")) ("∣")) -((("\\" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥")) -((("\\" "s" "i" "g" "m" "a")) ("σ")) -((("\\" "s" "i" "m")) ("∼")) -((("\\" "s" "i" "m" "e" "q")) ("≃")) -((("\\" "s" "m" "a" "l" "l" "a" "m" "a" "l" "g")) ("∐")) -((("\\" "s" "m" "a" "l" "l" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖")) -((("\\" "s" "m" "a" "l" "l" "s" "m" "i" "l" "e")) ("⌣")) -((("\\" "s" "m" "i" "l" "e")) ("⌣")) -((("\\" "s" "p" "a" "d" "e" "s" "u" "i" "t")) ("♠")) -((("\\" "s" "p" "h" "e" "r" "i" "c" "a" "l" "a" "n" "g" "l" "e")) ("∢")) -((("\\" "s" "q" "c" "a" "p")) ("⊓")) -((("\\" "s" "q" "c" "u" "p")) ("⊔")) -((("\\" "s" "q" "s" "u" "b" "s" "e" "t")) ("⊏")) -((("\\" "s" "q" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊑")) -((("\\" "s" "q" "s" "u" "p" "s" "e" "t")) ("⊐")) -((("\\" "s" "q" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊒")) -((("\\" "s" "q" "u" "a" "r" "e")) ("□")) -((("\\" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("⇝")) -((("\\" "s" "t" "a" "r")) ("⋆")) -((("\\" "s" "t" "r" "a" "i" "g" "h" "t" "p" "h" "i")) ("φ")) -((("\\" "s" "u" "b" "s" "e" "t")) ("⊂")) -((("\\" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊆")) -((("\\" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊆")) -((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q")) ("⊊")) -((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q" "q")) ("⊊")) -((("\\" "s" "u" "c" "c")) ("≻")) -((("\\" "s" "u" "c" "c" "a" "p" "p" "r" "o" "x")) ("≿")) -((("\\" "s" "u" "c" "c" "c" "u" "r" "l" "y" "e" "q")) ("≽")) -((("\\" "s" "u" "c" "c" "e" "q")) ("≽")) -((("\\" "s" "u" "c" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋩")) -((("\\" "s" "u" "c" "c" "n" "s" "i" "m")) ("⋩")) -((("\\" "s" "u" "c" "c" "s" "i" "m")) ("≿")) -((("\\" "s" "u" "m")) ("∑")) -((("\\" "s" "u" "p" "s" "e" "t")) ("⊃")) -((("\\" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊇")) -((("\\" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊇")) -((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q")) ("⊋")) -((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q" "q")) ("⊋")) -((("\\" "s" "u" "r" "d")) ("√")) -((("\\" "s" "w" "a" "r" "r" "o" "w")) ("↙")) -((("\\" "t" "a" "u")) ("τ")) -((("\\" "t" "h" "e" "r" "e" "f" "o" "r" "e")) ("∴")) -((("\\" "t" "h" "e" "t" "a")) ("θ")) -((("\\" "t" "h" "i" "c" "k" "a" "p" "p" "r" "o" "x")) ("≈")) -((("\\" "t" "h" "i" "c" "k" "s" "i" "m")) ("∼")) -((("\\" "t" "o")) ("→")) -((("\\" "t" "o" "p")) ("⊤")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e")) ("▵")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▿")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◃")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⊴")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "q")) ("≜")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▹")) -((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⊵")) -((("\\" "t" "w" "o" "h" "e" "a" "d" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↞")) -((("\\" "t" "w" "o" "h" "e" "a" "d" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↠")) -((("\\" "u" "l" "c" "o" "r" "n" "e" "r")) ("⌜")) -((("\\" "u" "p" "a" "r" "r" "o" "w")) ("↑")) -((("\\" "u" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↕")) -((("\\" "u" "p" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("↿")) -((("\\" "u" "p" "l" "u" "s")) ("⊎")) -((("\\" "u" "p" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("↾")) -((("\\" "u" "p" "s" "i" "l" "o" "n")) ("υ")) -((("\\" "u" "p" "u" "p" "a" "r" "r" "o" "w" "s")) ("⇈")) -((("\\" "u" "r" "c" "o" "r" "n" "e" "r")) ("⌝")) -((("\\" "u" "{" "i" "}")) ("ĭ")) -((("\\" "v" "D" "a" "s" "h")) ("⊨")) -((("\\" "v" "a" "r" "k" "a" "p" "p" "a")) ("ϰ")) -((("\\" "v" "a" "r" "p" "h" "i")) ("ϕ")) -((("\\" "v" "a" "r" "p" "i")) ("ϖ")) -((("\\" "v" "a" "r" "p" "r" "i" "m" "e")) ("′")) -((("\\" "v" "a" "r" "p" "r" "o" "p" "t" "o")) ("∝")) -((("\\" "v" "a" "r" "r" "h" "o")) ("ϱ")) -((("\\" "v" "a" "r" "s" "i" "g" "m" "a")) ("ς")) -((("\\" "v" "a" "r" "t" "h" "e" "t" "a")) ("ϑ")) -((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⊲")) -((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⊳")) -((("\\" "v" "d" "a" "s" "h")) ("⊢")) -((("\\" "v" "d" "o" "t" "s")) ("⋮")) -((("\\" "v" "e" "e")) ("∨")) -((("\\" "v" "e" "e" "b" "a" "r")) ("⊻")) -((("\\" "v" "e" "r" "t")) ("|")) -((("\\" "w" "e" "d" "g" "e")) ("∧")) -((("\\" "w" "p")) ("℘")) -((("\\" "w" "r")) ("≀")) -((("\\" "x" "i")) ("ξ")) -((("\\" "z" "e" "t" "a")) ("ζ")) -((("\\" "B" "b" "b" "{" "N" "}")) ("ℕ")) -((("\\" "B" "b" "b" "{" "P" "}")) ("ℙ")) -((("\\" "B" "b" "b" "{" "R" "}")) ("ℝ")) -((("\\" "B" "b" "b" "{" "Z" "}")) ("ℤ")) -((("-" "-")) ("–")) -((("-" "-" "-")) ("—")) -((("\\" " ")) (" ")) -((("\\" "\\")) ("\\")) -((("\\" "m" "u")) ("μ")) -((("\\" "r" "h" "o")) ("ρ")) -((("\\" "m" "a" "t" "h" "s" "c" "r" "{" "I" "}")) ("ℐ")) -((("\\" "S" "m" "i" "l" "e" "y")) ("☺")) -((("\\" "b" "l" "a" "c" "k" "s" "m" "i" "l" "e" "y")) ("☻")) -((("\\" "F" "r" "o" "w" "n" "y")) ("☹")) -((("\\" "L" "e" "t" "t" "e" "r")) ("✉")) -((("\\" "p" "e" "r" "m" "i" "l")) ("‰")) -((("\\" "r" "e" "g" "i" "s" "t" "e" "r" "e" "d")) ("®")) -((("\\" "c" "u" "r" "r" "e" "n" "c" "y")) ("¤")) -((("\\" "d" "h")) ("ð")) -((("\\" "D" "H")) ("Ð")) -((("\\" "t" "h")) ("þ")) -((("\\" "T" "H")) ("Þ")) -((("\\" "m" "i" "c" "r" "o")) ("µ")) -((("\\" "l" "n" "o" "t")) ("¬")) -((("\\" "o" "r" "d" "f" "e" "m" "i" "n" "i" "n" "e")) ("ª")) -((("\\" "o" "r" "d" "m" "a" "s" "c" "u" "l" "i" "n" "e")) ("º")) -((("\\" "l" "a" "m" "b" "d" "a" "b" "a" "r")) ("ƛ")) -((("\\" "c" "e" "l" "s" "i" "u" "s")) ("℃")) -((("\\" "l" "d" "q")) ("“")) -((("\\" "r" "d" "q")) ("”")) -((("\\" "m" "i" "n" "u" "s")) ("−")) -((("\\" "d" "e" "f" "s")) ("≙")) -((("\\" "l" "l" "b" "r" "a" "c" "k" "e" "t")) ("〚")) -((("\\" "r" "r" "b" "r" "a" "c" "k" "e" "t")) ("〛")) -((("\\" "l" "d" "a" "t" "a")) ("《")) -((("\\" "r" "d" "a" "t" "a")) ("》")) -((("\\" "g" "l" "q")) ("‚")) -((("\\" "g" "r" "q")) ("‘")) -((("\\" "g" "l" "q" "q")) ("„")) -((("\\" "\"" "`")) ("„")) -((("\\" "g" "r" "q" "q")) ("“")) -((("\\" "\"" "'")) ("“")) -((("\\" "f" "l" "q")) ("‹")) -((("\\" "f" "r" "q")) ("›")) -((("\\" "f" "l" "q" "q")) ("«")) -((("\\" "\"" "<")) ("«")) -((("\\" "f" "r" "q" "q")) ("»")) -((("\\" "\"" ">")) ("»")) -((("\\" "-")) ("")) -((("\\" "t" "e" "x" "t" "m" "u")) ("µ")) -((("\\" "t" "e" "x" "t" "f" "r" "a" "c" "t" "i" "o" "n" "s" "o" "l" "i" "d" "u" "s")) ("⁄")) -((("\\" "t" "e" "x" "t" "b" "i" "g" "c" "i" "r" "c" "l" "e")) ("⃝")) -((("\\" "t" "e" "x" "t" "m" "u" "s" "i" "c" "a" "l" "n" "o" "t" "e")) ("♪")) -((("\\" "t" "e" "x" "t" "d" "i" "e" "d")) ("✝")) -((("\\" "t" "e" "x" "t" "c" "o" "l" "o" "n" "m" "o" "n" "e" "t" "a" "r" "y")) ("₡")) -((("\\" "t" "e" "x" "t" "w" "o" "n")) ("₩")) -((("\\" "t" "e" "x" "t" "n" "a" "i" "r" "a")) ("₦")) -((("\\" "t" "e" "x" "t" "p" "e" "s" "o")) ("₱")) -((("\\" "t" "e" "x" "t" "l" "i" "r" "a")) ("₤")) -((("\\" "t" "e" "x" "t" "r" "e" "c" "i" "p" "e")) ("℞")) -((("\\" "t" "e" "x" "t" "i" "n" "t" "e" "r" "r" "o" "b" "a" "n" "g")) ("‽")) -((("\\" "t" "e" "x" "t" "p" "e" "r" "t" "e" "n" "t" "h" "o" "u" "s" "a" "n" "d")) ("‱")) -((("\\" "t" "e" "x" "t" "b" "a" "h" "t")) ("฿")) -((("\\" "t" "e" "x" "t" "n" "u" "m" "e" "r" "o")) ("№")) -((("\\" "t" "e" "x" "t" "d" "i" "s" "c" "o" "u" "n" "t")) ("⁒")) -((("\\" "t" "e" "x" "t" "e" "s" "t" "i" "m" "a" "t" "e" "d")) ("℮")) -((("\\" "t" "e" "x" "t" "o" "p" "e" "n" "b" "u" "l" "l" "e" "t")) ("◦")) -((("\\" "t" "e" "x" "t" "l" "q" "u" "i" "l" "l")) ("⁅")) -((("\\" "t" "e" "x" "t" "r" "q" "u" "i" "l" "l")) ("⁆")) -((("\\" "t" "e" "x" "t" "c" "i" "r" "c" "l" "e" "d" "P")) ("℗")) -((("\\" "t" "e" "x" "t" "r" "e" "f" "e" "r" "e" "n" "c" "e" "m" "a" "r" "k")) ("※")) -)) - -;; Local Variables: -;; mode: scheme -;; coding: utf-8 -;; End: diff --git a/ide/uim/coqide.scm b/ide/uim/coqide.scm deleted file mode 100644 index 62355ac2..00000000 --- a/ide/uim/coqide.scm +++ /dev/null @@ -1,277 +0,0 @@ -;;; coqide.scm -- Emacs-style Latin characters translation -;;; -;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ -;;; -;;; All rights reserved. -;;; -;;; Redistribution and use in source and binary forms, with or without -;;; modification, are permitted provided that the following conditions -;;; are met: -;;; 1. Redistributions of source code must retain the above copyright -;;; notice, this list of conditions and the following disclaimer. -;;; 2. Redistributions in binary form must reproduce the above copyright -;;; notice, this list of conditions and the following disclaimer in the -;;; documentation and/or other materials provided with the distribution. -;;; 3. Neither the name of authors nor the names of its contributors -;;; may be used to endorse or promote products derived from this software -;;; without specific prior written permission. -;;; -;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND -;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE -;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT -;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY -;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF -;;; SUCH DAMAGE. -;;;; - -;; This input method implements character composition rules for the -;; Latin letters used in European languages. The rules, defined in -;; the file coqide-rules.scm, have been adapted from GNU Emacs 22. - -(require "util.scm") -(require "rk.scm") -(require "coqide-rules.scm") -(require-custom "generic-key-custom.scm") -(require-custom "coqide-custom.scm") - -(define coqide-context-rec-spec - (append - context-rec-spec - '((on #f) - (rkc #f) - (show-cands #f)))) -(define-record 'coqide-context coqide-context-rec-spec) -(define coqide-context-new-internal coqide-context-new) - -(define (coqide-context-new id im) - (let ((lc (coqide-context-new-internal id im)) - (rkc (rk-context-new (symbol-value coqide-rules) #f #f))) - (coqide-context-set-widgets! lc coqide-widgets) - (coqide-context-set-rkc! lc rkc) - lc)) - -(define (coqide-current-translation lc) - (let ((rkc (coqide-context-rkc lc))) - (or (rk-peek-terminal-match rkc) - (and (not (null? (rk-context-seq rkc))) - (list (rk-pending rkc)))))) - -(define (coqide-current-string lc) - (let ((trans (coqide-current-translation lc))) - (if trans (car trans) ""))) - -(define (coqide-context-clear lc) - (rk-flush (coqide-context-rkc lc))) - -(define (coqide-context-flush lc) - (let ((str (coqide-current-string lc))) - (if (not (equal? str "")) (im-commit lc str)) - (coqide-context-clear lc))) - -(define (coqide-open-candidates-window lc height) - (if (coqide-context-show-cands lc) - (im-deactivate-candidate-selector lc)) - (im-activate-candidate-selector lc height height) - (im-select-candidate lc 0) - (coqide-context-set-show-cands! lc #t)) - -(define (coqide-close-candidates-window lc) - (if (coqide-context-show-cands lc) - (im-deactivate-candidate-selector lc)) - (coqide-context-set-show-cands! lc #f)) - -(define (coqide-update-preedit lc) - (if (coqide-context-on lc) - (let ((trans (coqide-current-translation lc)) - (ltrans 0)) - (im-clear-preedit lc) - (if trans - (begin (im-pushback-preedit lc - preedit-underline - (car trans)) - (set! ltrans (length trans)))) - (im-pushback-preedit lc - preedit-cursor - "") - (im-update-preedit lc) - (if (> ltrans 1) - (coqide-open-candidates-window lc ltrans) - (coqide-close-candidates-window lc))))) - -(define (coqide-prepare-activation lc) - (coqide-context-flush lc) - (coqide-update-preedit lc)) - -(register-action 'action_coqide_off - (lambda (lc) - (list - 'off - "a" - (N_ "CoqIDE mode off") - (N_ "CoqIDE composition off"))) - (lambda (lc) - (not (coqide-context-on lc))) - (lambda (lc) - (coqide-prepare-activation lc) - (coqide-context-set-on! lc #f))) - -(register-action 'action_coqide_on - (lambda (lc) - (list - 'on - "à" - (N_ "CoqIDE mode on") - (N_ "CoqIDE composition on"))) - (lambda (lc) - (coqide-context-on lc)) - (lambda (lc) - (coqide-prepare-activation lc) - (coqide-context-set-on! lc #t))) - -(define coqide-input-mode-actions - '(action_coqide_off action_coqide_on)) - -(define coqide-widgets '(widget_coqide_input_mode)) - -(define default-widget_coqide_input_mode 'action_coqide_on) - -(register-widget 'widget_coqide_input_mode - (activity-indicator-new coqide-input-mode-actions) - (actions-new coqide-input-mode-actions)) - -(define coqide-context-list '()) - -(define (coqide-init-handler id im arg) - (let ((lc (coqide-context-new id im))) - (set! coqide-context-list (cons lc coqide-context-list)) - lc)) - -(define (coqide-release-handler lc) - (let ((rkc (coqide-context-rkc lc))) - (set! coqide-context-list - ;; (delete lc coqide-context-list eq?) does not work - (remove (lambda (c) (eq? (coqide-context-rkc c) rkc)) - coqide-context-list)))) - -(define coqide-control-key? - (let ((shift-or-no-modifier? (make-key-predicate '("<Shift>" "")))) - (lambda (key key-state) - (not (shift-or-no-modifier? -1 key-state))))) - -(define (coqide-proc-on-state lc key key-state) - (let ((rkc (coqide-context-rkc lc)) - (cur-trans (coqide-current-translation lc))) - (cond - - ((or (coqide-off-key? key key-state) - (and coqide-esc-turns-off? (eq? key 'escape))) - (coqide-context-flush lc) - (if (eq? key 'escape) - (im-commit-raw lc)) - (coqide-context-set-on! lc #f) - (coqide-close-candidates-window lc) - (im-clear-preedit lc) - (im-update-preedit lc)) - - ((coqide-backspace-key? key key-state) - (if (not (rk-backspace rkc)) - (im-commit-raw lc))) - - ((coqide-control-key? key key-state) - (coqide-context-flush lc) - (im-commit-raw lc)) - - ((and (ichar-numeric? key) - (coqide-context-show-cands lc) - (let ((idx (- (numeric-ichar->integer key) 1))) - (if (= idx -1) (set! idx 9)) - (and (>= idx 0) (< idx (length cur-trans)) - (begin - (im-commit lc (nth idx cur-trans)) - (coqide-context-clear lc) - #t))))) - - (else - (let* ((key-str (if (symbol? key) - (symbol->string key) - (charcode->string key))) - (cur-seq (rk-context-seq rkc)) - (res (rk-push-key! rkc key-str)) - (new-seq (rk-context-seq rkc)) - (new-trans (coqide-current-translation lc))) - (if (equal? new-seq (cons key-str cur-seq)) - (if (not (or (rk-partial? rkc) (> (length new-trans) 1))) - (begin (im-commit lc (car (rk-peek-terminal-match rkc))) - (coqide-context-clear lc))) - (begin (if (not (null? cur-seq)) (im-commit lc (car cur-trans))) - (if (null? new-seq) (im-commit-raw lc))))))))) - -(define (coqide-proc-off-state lc key key-state) - (if (coqide-on-key? key key-state) - (coqide-context-set-on! lc #t) - (im-commit-raw lc))) - -(define (coqide-key-press-handler lc key key-state) - (if (coqide-context-on lc) - (coqide-proc-on-state lc key key-state) - (coqide-proc-off-state lc key key-state)) - (coqide-update-preedit lc)) - -(define (coqide-key-release-handler lc key key-state) - (if (or (ichar-control? key) - (not (coqide-context-on lc))) - ;; don't discard key release event for apps - (im-commit-raw lc))) - -(define (coqide-reset-handler lc) - (coqide-context-clear lc)) - -(define (coqide-get-candidate-handler lc idx accel-enum-hint) - (let* ((candidates (coqide-current-translation lc)) - (candidate (nth idx candidates))) - (list candidate (digit->string (+ idx 1)) ""))) - -;; Emacs does nothing on focus-out -;; TODO: this should be configurable -(define (coqide-focus-out-handler lc) - #f) - -(define (coqide-place-handler lc) - (coqide-update-preedit lc)) - -(define (coqide-displace-handler lc) - (coqide-context-flush lc) - (coqide-update-preedit lc)) - -(register-im - 'coqide - "" - "UTF-8" - coqide-im-name-label - coqide-im-short-desc - #f - coqide-init-handler - coqide-release-handler - context-mode-handler - coqide-key-press-handler - coqide-key-release-handler - coqide-reset-handler - coqide-get-candidate-handler - #f - context-prop-activate-handler - #f - #f - coqide-focus-out-handler - coqide-place-handler - coqide-displace-handler -) - -;; Local Variables: -;; mode: scheme -;; coding: utf-8 -;; End: diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b2b21925..fd230539 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) (*i*) open Pp @@ -602,7 +602,7 @@ let rec extern inctx scopes vars r = extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | RRef (loc,ref) -> - extern_global loc (implicits_of_global ref) + extern_global loc (select_stronger_impargs (implicits_of_global ref)) (extern_reference loc vars ref) | RVar (loc,id) -> CRef (Ident (loc,id)) @@ -655,7 +655,8 @@ let rec extern inctx scopes vars r = CRecord (loc, None, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> - extern_app loc inctx (implicits_of_global ref) + extern_app loc inctx + (select_stronger_impargs (implicits_of_global ref)) (Some ref,extern_reference rloc vars ref) args end | _ -> @@ -828,12 +829,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let subscopes = try list_skipn n (find_arguments_scope ref) with _ -> [] in let impls = - try list_skipn n (implicits_of_global ref) with _ -> [] in + let impls = + select_impargs_size + (List.length args) (implicits_of_global ref) in + try list_skipn n impls with _ -> [] in (if n = 0 then f else RApp (dummy_loc,f,args1)), args2, subscopes, impls | RApp (_,(RRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in - let impls = implicits_of_global ref in + let impls = + select_impargs_size + (List.length args) (implicits_of_global ref) in f, args, subscopes, impls | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], [] | _, None -> t, [], [], [] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3bf556f1..d918e94d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -41,7 +41,7 @@ type var_internalization_data = in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) identifier list * (* signature of impargs of the variable *) - Impargs.implicits_list * + Impargs.implicit_status list * (* subscopes of the args of the variable *) scope_name option list @@ -557,7 +557,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), impls, argsc, expl_impls + RVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Idset.mem id ids or List.mem id ltacvars @@ -598,7 +598,7 @@ let find_appl_head_data = function | RApp (_,RRef (_,ref),l) as x when l <> [] & Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in - x,list_skipn_at_least n (implicits_of_global ref), + x,List.map (drop_first_implicits n) (implicits_of_global ref), list_skipn_at_least n (find_arguments_scope ref),[] | x -> x,[],[],[] @@ -815,6 +815,7 @@ let subst_cases_pattern loc alias intern fullsubst scopes a = match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v with Not_found -> anomaly "Inconsistent substitution of recursive notation") + | AHole _ -> ([],[[], PatVar (loc,Anonymous)]) | t -> error_invalid_pattern_notation loc in aux alias fullsubst a @@ -1372,6 +1373,7 @@ let internalize sigma globalenv env allow_patvar lvar c = it_mkRLambda ibind body and intern_impargs c env l subscopes args = + let l = select_impargs_size (List.length args) l in let eargs, rargs = extract_explicit_arg l args in let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index acb13a8b..02a51e7e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) (*i*) open Names @@ -53,7 +53,7 @@ type var_internalization_data = identifier list * (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicits_list * (* signature of impargs of the variable *) + Impargs.implicit_status list * (** signature of impargs of the variable *) scope_name option list (* subscopes of the args of the variable *) (* A map of free variables to their implicit arguments and scopes *) diff --git a/interp/notation.ml b/interp/notation.ml index fe9d8b6d..8bf7ba21 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *) (*i*) open Util @@ -113,7 +113,7 @@ let subst_scope (subst,sc) = sc open Libobject -let discharge_scope (local,_,_ as o) = +let discharge_scope (_,(local,_,_ as o)) = if local then None else Some o let classify_scope (local,_,_ as o) = @@ -124,6 +124,7 @@ let (inScope,outScope) = cache_function = cache_scope; open_function = open_scope; subst_function = subst_scope; + discharge_function = discharge_scope; classify_function = classify_scope } let open_close_scope (local,opening,sc) = diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 53d26ec6..146da92c 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: mod_subst.ml 13414 2010-09-14 13:28:15Z glondu $ *) open Pp open Util @@ -638,7 +638,7 @@ let update_delta_resolver resolver1 resolver2 = Change_equiv_to_inline c -> Deltamap.add key (Inline (Some c)) res) | _ -> Deltamap.add key hint res - with not_found -> + with Not_found -> Deltamap.add key hint res in Deltamap.fold apply_res resolver1 empty_delta_resolver diff --git a/kernel/names.ml b/kernel/names.ml index 550c70b4..9f1becf7 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *) open Pp open Util @@ -108,7 +108,7 @@ let rec check_bound_mp = function | _ -> false let rec string_of_mp = function - | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")" + | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_uid uid (* | MPapp (mp1,mp2) -> "("^string_of_mp mp ^ " " ^ diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 00e8014f..46a469df 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reduction.ml 13354 2010-07-29 16:44:45Z barras $ *) +(* $Id: reduction.ml 13449 2010-09-22 19:31:50Z glondu $ *) open Util open Names @@ -176,9 +176,11 @@ type conv_pb = let sort_cmp pb s0 s1 cuniv = match (s0,s1) with - | (Prop c1, Prop c2) -> + | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Null or c2 = Pos then cuniv (* Prop <= Set *) else raise NotConvertible + | (Prop c1, Prop c2) -> + if c1 = c2 then cuniv else raise NotConvertible | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv | (Type u1, Type u2) -> assert (is_univ_variable u2); diff --git a/lib/flags.ml b/lib/flags.ml index de70b6a6..fc793780 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 13358 2010-07-29 23:10:17Z herbelin $ i*) +(*i $Id: flags.ml 13436 2010-09-19 10:18:18Z herbelin $ i*) let with_option o f x = let old = !o in o:=true; @@ -114,8 +114,7 @@ let browser_cmd_fmt = let is_standard_doc_url url = let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in - let wwwprefix = "http://coq.inria.fr/" in - let n = String.length wwwprefix in + let n = String.length Coq_config.wwwcoq in let n' = String.length Coq_config.wwwrefman in url = Coq_config.localwwwrefman || url = Coq_config.wwwrefman || diff --git a/lib/util.ml b/lib/util.ml index 851afc60..9a8c724f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 13357 2010-07-29 22:59:55Z herbelin $ *) +(* $Id: util.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp @@ -142,7 +142,7 @@ let string_string_contains ~where ~what = with Not_found -> false -let plural n s = if n>1 then s^"s" else s +let plural n s = if n<>1 then s^"s" else s let ordinal n = let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in @@ -1290,29 +1290,28 @@ let pr_vertical_list pr = function | [] -> str "none" ++ fnl () | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl () -let prvecti elem v = - let n = Array.length v in +(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs + [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) + +let prvecti_with_sep sep elem v = let rec pr i = if i = 0 then elem 0 v.(0) else - let r = pr (i-1) and e = elem i v.(i) in r ++ e + let r = pr (i-1) and s = sep () and e = elem i v.(i) in + r ++ s ++ e in + let n = Array.length v in if n = 0 then mt () else pr (n - 1) +(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) + +let prvecti elem v = prvecti_with_sep mt elem v + (* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) -let prvect_with_sep sep elem v = - let rec pr n = - if n = 0 then - elem v.(0) - else - let r = pr (n-1) and s = sep() and e = elem v.(n) in - r ++ s ++ e - in - let n = Array.length v in - if n = 0 then mt () else pr (n - 1) +let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v (* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *) diff --git a/lib/util.mli b/lib/util.mli index 00c73a1f..e5b5f8c6 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: util.mli 13357 2010-07-29 22:59:55Z herbelin $ i*) +(*i $Id: util.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) (*i*) open Pp @@ -330,7 +330,9 @@ val prlist_with_sep : val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val prvect_with_sep : - (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds + (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti_with_sep : + (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds diff --git a/library/impargs.ml b/library/impargs.ml index 2aff1dec..e695be3c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: impargs.ml 13499 2010-10-05 10:08:44Z herbelin $ *) open Util open Names @@ -29,14 +29,12 @@ open Namegen type implicits_flags = { auto : bool; (* automatic or manual only *) strict : bool; (* true = strict *) - strongly_strict : bool; (* true = strongly strict *) + strongly_strict : bool; (* true = strongly strict *) reversible_pattern : bool; contextual : bool; (* true = contextual *) maximal : bool } -(* les implicites sont stricts par défaut en v8 *) - let implicit_args = ref { auto = false; strict = true; @@ -198,6 +196,17 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = in frec true (env,1) m; acc +let rec is_rigid_head t = match kind_of_term t with + | Rel _ | Evar _ -> false + | Ind _ | Const _ | Var _ | Sort _ -> true + | Case (_,_,f,_) -> is_rigid_head f + | App (f,args) -> + (match kind_of_term f with + | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) + | _ -> is_rigid_head f) + | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ + | Prod _ | Meta _ | Cast _ -> assert false + (* calcule la liste des arguments implicites *) let find_displayed_name_in all avoid na b = @@ -207,6 +216,7 @@ let find_displayed_name_in all avoid na b = compute_displayed_name_in (RenamingElsewhereFor b) avoid na b let compute_implicits_gen strict strongly_strict revpat contextual all env t = + let rigid = ref true in let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with @@ -215,6 +225,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) | _ -> + rigid := is_rigid_head t; let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in if contextual then @@ -225,8 +236,66 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na b in let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in - Array.to_list v - | _ -> [] + !rigid, Array.to_list v + | _ -> true, [] + +let compute_implicits_flags env f all t = + compute_implicits_gen + (f.strict or f.strongly_strict) f.strongly_strict + f.reversible_pattern f.contextual all env t + +let compute_auto_implicits env flags enriching t = + if enriching then compute_implicits_flags env flags true t + else compute_implicits_gen false false false true true env t + +(* Extra information about implicit arguments *) + +type maximal_insertion = bool (* true = maximal contextual insertion *) +type force_inference = bool (* true = always infer, never turn into evar/subgoal *) + +type implicit_status = + (* None = Not implicit *) + (identifier * implicit_explanation * (maximal_insertion * force_inference)) option + +type implicit_side_condition = DefaultImpArgs | LessArgsThan of int + +type implicits_list = implicit_side_condition * implicit_status list + +let is_status_implicit = function + | None -> false + | _ -> true + +let name_of_implicit = function + | None -> anomaly "Not an implicit argument" + | Some (id,_,_) -> id + +let maximal_insertion_of = function + | Some (_,_,(b,_)) -> b + | None -> anomaly "Not an implicit argument" + +let force_inference_of = function + | Some (_, _, (_, b)) -> b + | None -> anomaly "Not an implicit argument" + +(* [in_ctx] means we know the expected type, [n] is the index of the argument *) +let is_inferable_implicit in_ctx n = function + | None -> false + | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p + | Some (_,DepFlex (Hyp p),_) -> false + | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q + | Some (_,DepRigid Conclusion,_) -> in_ctx + | Some (_,DepFlex Conclusion,_) -> false + | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx + | Some (_,Manual,_) -> true + +let positions_of_implicits (_,impls) = + let rec aux n = function + [] -> [] + | Some _ :: l -> n :: aux (n+1) l + | None :: l -> aux (n+1) l + in aux 1 impls + +(* Manage user-given implicit arguments *) let rec prepare_implicits f = function | [] -> [] @@ -236,11 +305,6 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let compute_implicits_flags env f all t = - compute_implicits_gen - (f.strict or f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env t - let set_implicit id imp insmax = (id,(match imp with None -> Manual | Some imp -> imp),insmax) @@ -249,11 +313,20 @@ let rec assoc_by_pos k = function | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl | [] -> raise Not_found -let compute_manual_implicits env flags t enriching l = - let autoimps = - if enriching then compute_implicits_flags env flags true t - else compute_implicits_gen false false false true true env t in - let n = List.length autoimps in +let check_correct_manual_implicits autoimps l = + List.iter (function + | ExplByName id,(b,fi,forced) -> + if not forced then + error ("Wrong or non-dependent implicit argument name: "^(string_of_id id)^".") + | ExplByPos (i,_id),_t -> + if i<1 or i>List.length autoimps then + error ("Bad implicit argument number: "^(string_of_int i)^".") + else + errorlabstrm "" + (str "Cannot set implicit argument number " ++ int i ++ + str ": it has no name.")) l + +let set_manual_implicits env flags enriching autoimps l = let try_forced k l = try let (id, (b, fi, fo)), l' = assoc_by_pos k l in @@ -264,7 +337,7 @@ let compute_manual_implicits env flags t enriching l = with Not_found -> l, None in if not (list_distinct l) then - error ("Some parameters are referred more than once"); + error ("Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> @@ -287,81 +360,28 @@ let compute_manual_implicits env flags t enriching l = forced :: merge (k+1) l' imps | [] when l = [] -> [] | [] -> - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) - | ExplByPos (i,_id),_t -> - if i<1 or i>n then - error ("Bad implicit argument number: "^(string_of_int i)) - else - errorlabstrm "" - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name")) - l; [] + check_correct_manual_implicits autoimps l; + [] in merge 1 l autoimps -let const v _ = v - -let compute_implicits_auto env f manual t = +let compute_semi_auto_implicits env f manual t = match manual with | [] -> - if not f.auto then [] - else let l = compute_implicits_flags env f false t in - prepare_implicits f l - | _ -> compute_manual_implicits env f t f.auto manual - -let compute_implicits env t = compute_implicits_auto env !implicit_args [] t - -type maximal_insertion = bool (* true = maximal contextual insertion *) -type force_inference = bool (* true = always infer, never turn into evar/subgoal *) - -type implicit_status = - (* None = Not implicit *) - (identifier * implicit_explanation * (maximal_insertion * force_inference)) option - -type implicits_list = implicit_status list - -let is_status_implicit = function - | None -> false - | _ -> true - -let name_of_implicit = function - | None -> anomaly "Not an implicit argument" - | Some (id,_,_) -> id - -let maximal_insertion_of = function - | Some (_,_,(b,_)) -> b - | None -> anomaly "Not an implicit argument" + if not f.auto then [DefaultImpArgs, []] + else let _,l = compute_implicits_flags env f false t in + [DefaultImpArgs, prepare_implicits f l] + | _ -> + let _,autoimpls = compute_auto_implicits env f f.auto t in + [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] -let force_inference_of = function - | Some (_, _, (_, b)) -> b - | None -> anomaly "Not an implicit argument" - -(* [in_ctx] means we know the expected type, [n] is the index of the argument *) -let is_inferable_implicit in_ctx n = function - | None -> false - | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p - | Some (_,DepFlex (Hyp p),_) -> false - | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q - | Some (_,DepRigid Conclusion,_) -> in_ctx - | Some (_,DepFlex Conclusion,_) -> false - | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx - | Some (_,Manual,_) -> true - -let positions_of_implicits = - let rec aux n = function - [] -> [] - | Some _ :: l -> n :: aux (n+1) l - | None :: l -> aux (n+1) l - in aux 1 +let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t (*s Constants. *) let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_implicits_auto env flags manual (Typeops.type_of_constant env cst) + compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -381,9 +401,9 @@ let compute_mib_implicits flags manual kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,compute_implicits_auto env flags manual ar), + ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c)) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets @@ -398,7 +418,7 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - compute_implicits_auto env flags manual ty + compute_semi_auto_implicits env flags manual ty (* Implicits of a global reference. *) @@ -412,24 +432,21 @@ let compute_global_implicits flags manual = function (* Merge a manual explicitation with an implicit_status list *) -let merge_impls oldimpls newimpls = - let (before, news), olds = - let len = List.length newimpls - List.length oldimpls in - if len >= 0 then list_split_at len newimpls, oldimpls - else - let before, after = list_split_at (-len) oldimpls in - (before, newimpls), after - in - before @ (List.map2 (fun orig ni -> - match orig with - | Some (_, Manual, _) -> orig - | _ -> ni) olds news) +let merge_impls (cond,oldimpls) (_,newimpls) = + let oldimpls,usersuffiximpls = list_chop (List.length newimpls) oldimpls in + cond, (List.map2 (fun orig ni -> + match orig with + | Some (_, Manual, _) -> orig + | _ -> ni) oldimpls newimpls)@usersuffiximpls + +let merge_impls_list oldimpls newimpls = + merge_impls oldimpls newimpls (* Caching implicits *) type implicit_interactive_request = | ImplAuto - | ImplManual of implicit_status list + | ImplManual of int type implicit_discharge_request = | ImplLocal @@ -441,7 +458,7 @@ type implicit_discharge_request = let implicits_table = ref Refmap.empty let implicits_of_global ref = - try Refmap.find ref !implicits_table with Not_found -> [] + try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = implicits_table := Refmap.add ref imps !implicits_table @@ -467,23 +484,35 @@ let section_segment_of_reference = function section_segment_of_mutual_inductive kn | _ -> [] +let adjust_side_condition p = function + | LessArgsThan n -> LessArgsThan (n+p) + | DefaultImpArgs -> DefaultImpArgs + +let add_section_impls vars extra_impls (cond,impls) = + let p = List.length vars - List.length extra_impls in + adjust_side_condition p cond, extra_impls @ impls + let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> let vars = section_segment_of_reference ref in let ref' = if isVarRef ref then ref else pop_global_reference ref in - let l' = [ref', impls_of_context vars @ snd (List.hd l)] in + let extra_impls = impls_of_context vars in + let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') | ImplConstant (con,flags) -> let con' = pop_con con in - let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in + let vars = section_segment_of_constant con in + let extra_impls = impls_of_context vars in + let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplConstant (con',flags),l') | ImplMutualInductive (kn,flags) -> let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in + let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), - impls_of_context vars @ l)) l + List.map (add_section_impls vars extra_impls) l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') @@ -493,13 +522,13 @@ let rebuild_implicits (req,l) = | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in let newimpls = compute_constant_implicits flags [] con in - req, [ConstRef con, merge_impls oldimpls newimpls] + req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags [] kn in let rec aux olds news = match olds, news with | (_, oldimpls) :: old, (gr, newimpls) :: tl -> - (gr, merge_impls oldimpls newimpls) :: aux old tl + (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl | [], [] -> [] | _, _ -> assert false in req, aux l newimpls @@ -510,17 +539,16 @@ let rebuild_implicits (req,l) = | ImplAuto -> let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags [] ref in - [ref,merge_impls oldimpls newimpls] - | ImplManual m -> + [ref,List.map2 merge_impls oldimpls newimpls] + | ImplManual userimplsize -> let oldimpls = snd (List.hd l) in - let auto = - if flags.auto then - let newimpls = compute_global_implicits flags [] ref in - merge_impls oldimpls newimpls - else oldimpls - in - let l' = merge_impls auto m in - [ref,l'] + if flags.auto then + let newimpls = List.hd (compute_global_implicits flags [] ref) in + let p = List.length (snd newimpls) - userimplsize in + let newimpls = on_snd (list_firstn p) newimpls in + [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] + else + [ref,oldimpls] let classify_implicits (req,_ as obj) = if req = ImplLocal then Dispose else Substitute obj @@ -566,23 +594,58 @@ let declare_mib_implicits kn = type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) let compute_implicits_with_manual env typ enriching l = - compute_manual_implicits env !implicit_args typ enriching l + let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in + set_manual_implicits env !implicit_args enriching autoimpls l + +let check_inclusion l = + (* Check strict inclusion *) + let rec aux = function + | n1::(n2::_ as nl) -> + if n1 <= n2 then + error "Sequences of implicit arguments must be of different lengths"; + aux nl + | _ -> () in + aux (List.map (fun (imps,_) -> List.length imps) l) + +let check_rigidity isrigid = + if not isrigid then + errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in let t = Global.type_of_global ref in let enriching = Option.default flags.auto enriching in - let l' = compute_manual_implicits env flags t enriching l in + let isrigid,autoimpls = compute_auto_implicits env flags enriching t in + let l' = match l with + | [] -> assert false + | [l] -> + [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + | _ -> + check_rigidity isrigid; + let l = List.map (fun imps -> (imps,List.length imps)) l in + let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in + check_inclusion l; + let nargs = List.length autoimpls in + List.map (fun (imps,n) -> + (LessArgsThan (nargs-n), + set_manual_implicits env flags enriching autoimpls imps)) l in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual l') + else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = if l = [] then () - else declare_manual_implicits local ref ?enriching l + else declare_manual_implicits local ref ?enriching [l] + +let extract_impargs_data impls = + let rec aux p = function + | (DefaultImpArgs, imps)::_ -> [None,imps] + | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l + | [] -> [] in + aux 0 impls let lift_implicits n = List.map (fun x -> @@ -590,6 +653,27 @@ let lift_implicits n = ExplByPos (k, id) -> ExplByPos (k + n, id), snd x | _ -> x) +let make_implicits_list l = [DefaultImpArgs, l] + +let rec drop_first_implicits p l = + if p = 0 then l else match l with + | _,[] as x -> x + | DefaultImpArgs,imp::impls -> + drop_first_implicits (p-1) (DefaultImpArgs,impls) + | LessArgsThan n,imp::impls -> + let n = if is_status_implicit imp then n-1 else n in + drop_first_implicits (p-1) (LessArgsThan n,impls) + +let rec select_impargs_size n = function + | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) + | [_, impls] | (DefaultImpArgs, impls)::_ -> impls + | (LessArgsThan p, impls)::l -> + if n <= p then impls else select_impargs_size n l + +let rec select_stronger_impargs = function + | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) + | (_,impls)::_ -> impls + (*s Registration as global tables *) let init () = implicits_table := Refmap.empty diff --git a/library/impargs.mli b/library/impargs.mli index 1c27d9f5..0b0ae544 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: impargs.mli 13499 2010-10-05 10:08:44Z herbelin $ i*) (*i*) open Names @@ -51,7 +51,10 @@ type implicit_explanation = | Manual type implicit_status = (identifier * implicit_explanation * (bool * bool)) option -type implicits_list = implicit_status list + +type implicit_side_condition + +type implicits_list = implicit_side_condition * implicit_status list val is_status_implicit : implicit_status -> bool val is_inferable_implicit : bool -> int -> implicit_status -> bool @@ -63,7 +66,7 @@ val positions_of_implicits : implicits_list -> int list (* Computation of the positions of arguments automatically inferable for an object of the given type in the given env *) -val compute_implicits : env -> types -> implicits_list +val compute_implicits : env -> types -> implicits_list list (* A [manual_explicitation] is a tuple of a positional or named explicitation with maximal insertion, force inference and force usage flags. Forcing usage makes @@ -71,7 +74,7 @@ val compute_implicits : env -> types -> implicits_list type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) val compute_implicits_with_manual : env -> types -> bool -> - manual_explicitation list -> implicits_list + manual_explicitation list -> implicit_status list (*s Computation of implicits (done using the global environment). *) @@ -88,22 +91,33 @@ val declare_implicits : bool -> global_reference -> unit Unsets implicits if [l] is empty. *) val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_explicitation list -> unit + manual_explicitation list list -> unit (* If the list is empty, do nothing, otherwise declare the implicits. *) val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> manual_explicitation list -> unit -val implicits_of_global : global_reference -> implicits_list +val implicits_of_global : global_reference -> implicits_list list + +val extract_impargs_data : + implicits_list list -> ((int * int) option * implicit_status list) list val lift_implicits : int -> manual_explicitation list -> manual_explicitation list val merge_impls : implicits_list -> implicits_list -> implicits_list +val make_implicits_list : implicit_status list -> implicits_list list + +val drop_first_implicits : int -> implicits_list -> implicits_list + +val select_impargs_size : int -> implicits_list list -> implicit_status list + +val select_stronger_impargs : implicits_list list -> implicit_status list + type implicit_interactive_request = | ImplAuto - | ImplManual of implicit_status list + | ImplManual of int type implicit_discharge_request = | ImplLocal diff --git a/library/states.ml b/library/states.ml index 3af2bcd7..5fc26045 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: states.ml 13431 2010-09-18 08:15:29Z herbelin $ *) open System @@ -30,12 +30,12 @@ let (extern_state,intern_state) = (* Rollback. *) -let with_heavy_rollback f x = +let with_heavy_rollback f h x = let st = freeze () in try f x with reraise -> - (unfreeze st; raise reraise) + let e = h reraise in (unfreeze st; raise e) let with_state_protection f x = let st = freeze () in diff --git a/library/states.mli b/library/states.mli index 198e1632..b6bdff8b 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: states.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: states.mli 13431 2010-09-18 08:15:29Z herbelin $ i*) (*s States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by @@ -24,7 +24,7 @@ val unfreeze : state -> unit state of the whole system as it was before the evaluation if an exception is raised. *) -val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b +val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b (*s [with_state_protection f x] applies [f] to [x] and restores the state of the whole system as it was before the evaluation of f *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1f5a6cf9..304640b2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp @@ -549,7 +549,7 @@ GEXTEND Gram (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = OPT [ "["; l = LIST0 implicit_name; "]" -> + pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> VernacDeclareImplicits (use_section_locality (),qid,pos) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index cc48c84f..a89594c2 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -10,7 +10,7 @@ (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with * ast-based camlp4 *) -(*i $Id: lexer.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: lexer.ml4 13521 2010-10-10 21:59:00Z herbelin $ i*) open Pp open Util @@ -147,7 +147,7 @@ let lookup_utf8_tail c cs = | _ -> error_utf8 cs in try classify_unicode unicode, n - with UnsupportedUtf8 -> error_unsupported_unicode_character n cs + with UnsupportedUtf8 -> njunk n cs; error_unsupported_unicode_character n cs let lookup_utf8 cs = match Stream.peek cs with diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ff35be57..b5e0cc4a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: ppvernac.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Names @@ -847,13 +847,15 @@ let rec pr_vernac = function (pr_locality local ++ str"Notation " ++ pr_lident id ++ prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (local,q,None) -> + | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ pr_smart_global q) - | VernacDeclareImplicits (local,q,Some imps) -> + | VernacDeclareImplicits (local,q,impls) -> hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ spc() ++ pr_smart_global q ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + prlist_with_sep spc (fun imps -> + str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + impls) | VernacReserve bl -> let n = List.length (List.flatten (List.map fst bl)) in hov 2 (str"Implicit Type" ++ diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 9c39e57e..cf83c72a 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -51,39 +51,25 @@ type object_pr = { let gallina_print_module = print_module let gallina_print_modtype = print_modtype -(*********************) -(** Basic printing *) - -let print_basename sp = pr_global (ConstRef sp) +(**************) +(** Utilities *) let print_closed_sections = ref false -let with_line_skip p = if ismt p then mt() else (fnl () ++ p) +let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) ++ fnl() -(********************************) -(** Printing implicit arguments *) +let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l -let conjugate_to_be = function [_] -> "is" | _ -> "are" +let blankline = mt() (* add a blank sentence in the list of infos *) -let pr_implicit imp = pr_id (name_of_implicit imp) +let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " -let print_impl_args_by_name max = function - | [] -> mt () - | impls -> - hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ - prlist_with_sep pr_comma pr_implicit impls ++ spc() ++ - str (conjugate_to_be impls) ++ str" implicit" ++ - (if max then strbrk " and maximally inserted" else mt())) ++ fnl() +let int_or_no n = if n=0 then str "no" else int n -let print_impl_args l = - let imps = List.filter is_status_implicit l in - let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = list_subtract imps maximps in - print_impl_args_by_name false nonmaximps ++ - print_impl_args_by_name true maximps +(*******************) +(** Basic printing *) -(*********************) -(** Printing Scopes *) +let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global ref in @@ -92,16 +78,49 @@ let print_ref reduce ref = let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ in it_mkProd_or_LetIn ccl ctx else typ in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl () + hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) -let print_argument_scopes = function - | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl() - | l when not (List.for_all ((=) None) l) -> - hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ - str "]") ++ fnl() - | _ -> mt() +(********************************) +(** Printing implicit arguments *) + +let conjugate_verb_to_be = function [_] -> "is" | _ -> "are" + +let pr_impl_name imp = pr_id (name_of_implicit imp) + +let print_impargs_by_name max = function + | [] -> [] + | impls -> + [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ + str (conjugate_verb_to_be impls) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt()))] + +let print_one_impargs_list l = + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = list_subtract imps maximps in + print_impargs_by_name false nonmaximps @ + print_impargs_by_name true maximps + +let print_impargs_list prefix l = + let l = extract_impargs_data l in + List.flatten (List.map (fun (cond,imps) -> + match cond with + | None -> + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) + | Some (n1,n2) -> + [v 2 (prlist_with_sep cut (fun x -> x) + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if n1 = n2 then int_or_no n2 else + if n1 = 0 then str "less than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (plural n2 " argument") ++ str ":"; + v 0 (prlist_with_sep cut (fun x -> x) + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) l) let need_expansion impl ref = let typ = Global.type_of_global ref in @@ -111,6 +130,33 @@ let need_expansion impl ref = let _,lastimpl = list_chop nprods impl in List.filter is_status_implicit lastimpl <> [] +let print_impargs ref = + let ref = Smartlocate.smart_global ref in + let impl = implicits_of_global ref in + let has_impl = impl <> [] in + (* Need to reduce since implicits are computed with products flattened *) + pr_infos_list + ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref; + blankline ] @ + (if has_impl then print_impargs_list (mt()) impl + else [str "No implicit arguments"])) + +(*********************) +(** Printing Scopes *) + +let print_argument_scopes prefix = function + | [Some sc] -> + [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] + | l when not (List.for_all ((=) None) l) -> + [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ + prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ + str "]")] + | _ -> [] + +(*********************) +(** Printing Opacity *) + type opacity = | FullyOpaque | TransparentMaybeOpacified of Conv_oracle.level @@ -128,8 +174,9 @@ let opacity env = function let print_opacity ref = match opacity (Global.env()) ref with - | None -> mt () - | Some s -> pr_global ref ++ str " is " ++ + | None -> [] + | Some s -> + [pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> @@ -139,38 +186,45 @@ let print_opacity ref = | TransparentMaybeOpacified (Conv_oracle.Level n) -> "transparent (with expansion weight "^string_of_int n^")" | TransparentMaybeOpacified Conv_oracle.Expand -> - "transparent (with minimal expansion weight)") ++ fnl() + "transparent (with minimal expansion weight)")] + +(*******************) +(* *) let print_name_infos ref = - let impl = implicits_of_global ref in + let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in - let type_for_implicit = - if need_expansion impl ref then + let type_info_for_implicit = + if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) - str "Expanded type for implicit arguments" ++ fnl () ++ - print_ref true ref ++ fnl() - else mt() in - type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes + [str "Expanded type for implicit arguments"; + print_ref true ref; blankline] + else + [] in + type_info_for_implicit @ + print_impargs_list (mt()) impls @ + print_argument_scopes (mt()) scopes let print_id_args_data test pr id l = if List.exists test l then - str"For " ++ pr_id id ++ str": " ++ pr l + pr (str "For " ++ pr_id id) l else - mt() + [] let print_args_data_of_inductive_ids get test pr sp mipv = - prvecti + List.flatten (Array.to_list (Array.mapi (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++ - prvecti + print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @ + List.flatten (Array.to_list (Array.mapi (fun j idc -> print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) - mip.mind_consnames) - mipv + mip.mind_consnames))) + mipv)) let print_inductive_implicit_args = print_args_data_of_inductive_ids - implicits_of_global is_status_implicit print_impl_args + implicits_of_global (fun l -> positions_of_implicits l <> []) + print_impargs_list let print_inductive_argument_scopes = print_args_data_of_inductive_ids @@ -365,7 +419,7 @@ let gallina_print_inductive sp = else pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ with_line_skip - (print_inductive_implicit_args sp mipv ++ + (print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) let print_named_decl id = @@ -666,16 +720,19 @@ let print_opaque_name qid = print_named_decl (id,c,ty) let print_about_any k = - begin match k with + match k with | Term ref -> - print_ref false ref ++ fnl () ++ print_name_infos ref ++ - print_opacity ref + pr_infos_list + ([print_ref false ref; blankline] @ + print_name_infos ref @ + print_opacity ref @ + [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> - print_syntactic_def kn + v 0 ( + print_syntactic_def kn ++ + hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl() | Dir _ | ModuleType _ | Undefined _ -> - mt () end - ++ - hov 0 (str "Expands to: " ++ pr_located_qualid k) + hov 0 (pr_located_qualid k) ++ fnl() let print_about = function | Genarg.ByNotation (loc,ntn,sc) -> @@ -685,15 +742,6 @@ let print_about = function | Genarg.AN ref -> print_about_any (locate_any_name ref) -let print_impargs ref = - let ref = Smartlocate.smart_global ref in - let impl = implicits_of_global ref in - let has_impl = List.filter is_status_implicit impl <> [] in - (* Need to reduce since implicits are computed with products flattened *) - print_ref (need_expansion impl ref) ref ++ fnl() ++ - (if has_impl then print_impl_args impl - else (str "No implicit arguments" ++ fnl ())) - let unfold_head_fconst = let rec unfrec k = match kind_of_term k with | Const cst -> constant_value (Global.env ()) cst @@ -771,7 +819,7 @@ let print_canonical_projections () = open Typeclasses let pr_typeclass env t = - print_ref false t.cl_impl + print_ref false t.cl_impl ++ fnl () let print_typeclasses () = let env = Global.env () in @@ -780,7 +828,7 @@ let print_typeclasses () = let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) - print_ref false (instance_impl i) + print_ref false (instance_impl i) ++ fnl () let print_all_instances () = let env = Global.env () in diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index d7f83b63..5704f54e 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: prettyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: prettyp.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) (*i*) open Pp @@ -26,7 +26,6 @@ open Genarg val assumptions_for_print : name list -> Termops.names_context val print_closed_sections : bool ref -val print_impl_args : Impargs.implicits_list -> std_ppcmds val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option val print_full_context : unit -> std_ppcmds @@ -46,12 +45,6 @@ val print_opaque_name : reference -> std_ppcmds val print_about : reference or_by_notation -> std_ppcmds val print_impargs : reference or_by_notation -> std_ppcmds -(*i -val print_extracted_name : identifier -> std_ppcmds -val print_extraction : unit -> std_ppcmds -val print_extracted_vars : unit -> std_ppcmds -i*) - (* Pretty-printing functions for classes and coercions *) val print_graph : unit -> std_ppcmds val print_classes : unit -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index c9f27678..cf0050a5 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: printer.ml 13390 2010-09-02 08:03:01Z herbelin $ *) open Pp open Util @@ -263,7 +263,7 @@ let pr_predicate pr_elt (b, elts) = else if elts = [] then str"none" else pr_elts -let pr_cpred p = pr_predicate pr_con (Cpred.elements p) +let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p) let pr_transparent_state (ids, csts) = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4171aceb..82b4143e 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *) (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) @@ -339,6 +339,28 @@ and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 | other -> applistc (constr_of_term other) l +let rec canonize_name c = + let func = canonize_name in + match kind_of_term c with + | Const kn -> + let canon_const = constant_of_kn (canonical_con kn) in + (mkConst canon_const) + | Ind (kn,i) -> + let canon_mind = mind_of_kn (canonical_mind kn) in + (mkInd (canon_mind,i)) + | Construct ((kn,i),j) -> + let canon_mind = mind_of_kn (canonical_mind kn) in + mkConstruct ((canon_mind,i),j) + | Prod (na,t,ct) -> + mkProd (na,func t, func ct) + | Lambda (na,t,ct) -> + mkLambda (na, func t,func ct) + | LetIn (na,b,t,ct) -> + mkLetIn (na, func b,func t,func ct) + | App (ct,l) -> + mkApp (func ct,array_smartmap func l) + | _ -> c + (* rebuild a term from a pattern and a substitution *) let build_subst uf subst = @@ -366,6 +388,7 @@ let rec add_term state t= Not_found -> let b=next uf in let typ = pf_type_of state.gls (constr_of_term t) in + let typ = canonize_name typ in let new_node= match t with Symb _ | Product (_,_) -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b7358121..ca1a9085 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -74,11 +74,21 @@ let rec decompose_term env sigma t= decompose_term env sigma a), decompose_term env sigma b) | Construct c-> - let (oib,_)=Global.lookup_inductive (fst c) in - let nargs=mis_constructor_nargs_env env c in - Constructor {ci_constr=c; + let (mind,i_ind),i_con = c in + let canon_mind = mind_of_kn (canonical_mind mind) in + let canon_ind = canon_mind,i_ind in + let (oib,_)=Global.lookup_inductive (canon_ind) in + let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in + Constructor {ci_constr= (canon_ind,i_con); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} + | Ind c -> + let mind,i_ind = c in + let canon_mind = mind_of_kn (canonical_mind mind) in + let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) + | Const c -> + let canon_const = constant_of_kn (canonical_con c) in + (Symb (mkConst canon_const)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) @@ -106,7 +116,7 @@ let rec pattern_of_constr env sigma c = | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> let b =pop _b in let pa,sa = pattern_of_constr env sigma a in - let pb,sb = pattern_of_constr env sigma (pop b) in + let pb,sb = pattern_of_constr env sigma b in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in PApp(Product (sort_a,sort_b), @@ -143,27 +153,27 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with - Prod (_,atom,ff) -> + Prod (id,atom,ff) -> if eq_constr ff (Lazy.force _False) then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts - else - quantified_atom_of_constr env sigma (succ nrels) ff - | _ -> + else + quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff + | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with - | Prod (_,atom,ff) -> + | Prod (id,atom,ff) -> if eq_constr ff (Lazy.force _False) then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) else begin - try - quantified_atom_of_constr env sigma 1 ff + try + quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index ca72f873..8dc512fa 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) open Pp open Util @@ -177,6 +177,10 @@ let mktable autoclean = let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content = mktable false +let get_mpfiles_content mp = + try get_mpfiles_content mp + with Not_found -> failwith "get_mpfiles_content" + (*s The list of external modules that will be opened initially *) let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear = @@ -223,11 +227,13 @@ let pop_visible, push_visible, get_visible = let vis = ref [] in register_cleanup (fun () -> vis := []); let pop () = - let v = List.hd !vis in - (* we save the 1st-level-content of MPfile for later use *) - if get_phase () = Impl && modular () && is_modfile v.mp - then add_mpfiles_content v.mp v.content; - vis := List.tl !vis + match !vis with + | [] -> assert false + | v :: vl -> + vis := vl; + (* we save the 1st-level-content of MPfile for later use *) + if get_phase () = Impl && modular () && is_modfile v.mp + then add_mpfiles_content v.mp v.content and push mp mps = vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis and get () = !vis @@ -306,8 +312,8 @@ let rec mp_renaming_fun mp = match mp with let s = modular_rename Mod (id_of_mbid mbid) in if not (params_ren_mem mp) then [s] else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i] - | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *) | MPfile _ -> + assert (modular ()); (* see [at_toplevel] above *) assert (get_phase () = Pre); let current_mpfile = (list_last (get_visible ())).mp in if mp <> current_mpfile then mpfiles_add mp; @@ -402,27 +408,28 @@ let visible_clash_dbg mp0 ks = let opened_libraries () = if not (modular ()) then [] else - let used = mpfiles_list () in - let rec check_elsewhere avoid = function - | [] -> [] - | mp :: mpl -> - let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in - if List.exists clash avoid - then check_elsewhere avoid mpl - else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl + let used_files = mpfiles_list () in + let used_ks = List.map (fun mp -> Mod,string_of_modfile mp) used_files in + (* By default, we open all used files. Ambiguities will be resolved later + by using qualified names. Nonetheless, we don't open any file A that + contains an immediate submodule A.B hiding another file B : otherwise, + after such an open, there's no unambiguous way to refer to objects of B. *) + let to_open = + List.filter + (fun mp -> + not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks)) + used_files in - let opened = check_elsewhere [] used in mpfiles_clear (); - List.iter mpfiles_add opened; - opened + List.iter mpfiles_add to_open; + mpfiles_list () (*s On-the-fly qualification issues for both monolithic or modular extraction. *) -(* First, a function that factorize the printing of both [global_reference] - and module names for ocaml. When [k=Mod] then [olab=None], otherwise it - contains the label of the reference to print. - [rls] is the string list giving the qualified name, short name at the end. - Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *) +(* [pp_ocaml_gen] below is a function that factorize the printing of both + [global_reference] and module names for ocaml. When [k=Mod] then [olab=None], + otherwise it contains the label of the reference to print. + [rls] is the string list giving the qualified name, short name at the end. *) (* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we cannot do that. So, if [t] gets hidden and we need a long name for it, @@ -471,18 +478,21 @@ let pp_ocaml_bound base rls = (* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *) let pp_ocaml_extern k base rls = match rls with - | [] | [_] -> assert false + | [] -> assert false | base_s :: rls' -> - let k's = fstlev_ks k rls' in - if modular () && (mpfiles_mem base) && - (not (mpfiles_clash base k's)) && - (not (visible_clash base k's)) - then (* Standard situation of an object in another file: *) - (* Thanks to the "open" of this file we remove its name *) + if (not (modular ())) (* Pseudo qualification with "" *) + || (rls' = []) (* Case of a file A.v used as a module later *) + || (not (mpfiles_mem base)) (* Module not opened *) + || (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *) + || (visible_clash base (fstlev_ks k rls')) (* Local conflict *) + then + (* We need to fully qualify. Last clash situation is unsupported *) + match visible_clash_dbg base (Mod,base_s) with + | None -> dottify rls + | Some (mp,l) -> error_module_clash base (MPdot (mp,l)) + else + (* Standard situation : object in an opened file *) dottify rls' - else match visible_clash_dbg base (Mod,base_s) with - | None -> dottify rls - | Some (mp,l) -> error_module_clash base (MPdot (mp,l)) (* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 58d8fcb1..c5929392 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) open Term open Declarations @@ -69,7 +69,7 @@ module type VISIT = sig (* Add kernel_name / constant / reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_kn : mutual_inductive -> unit + val add_ind : mutual_inductive -> unit val add_con : constant -> unit val add_ref : global_reference -> unit val add_decl_deps : ml_decl -> unit @@ -77,31 +77,35 @@ module type VISIT = sig (* Test functions: is a particular object a needed dependency for the current extraction ? *) - val needed_kn : mutual_inductive -> bool + val needed_ind : mutual_inductive -> bool val needed_con : constant -> bool val needed_mp : module_path -> bool end module Visit : VISIT = struct (* What used to be in a single KNset should now be split into a KNset - (for inductives and modules names) and a Cset for constants + (for inductives and modules names) and a Cset_env for constants (and still the remaining MPset) *) type must_visit = - { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t } + { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t } (* the imperative internal visit lists *) - let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty } + let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty } (* the accessor functions *) - let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty - let needed_kn kn = Mindset.mem kn v.kn - let needed_con c = Cset.mem c v.con + let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty + let needed_ind i = KNset.mem (user_mind i) v.ind + let needed_con c = KNset.mem (user_con c) v.con let needed_mp mp = MPset.mem mp v.mp let add_mp mp = check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp - let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn) - let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) + let add_ind i = + let kn = user_mind i in + v.ind <- KNset.add kn v.ind; add_mp (modpath kn) + let add_con c = + let kn = user_con c in + v.con <- KNset.add kn v.con; add_mp (modpath kn) let add_ref = function | ConstRef c -> add_con c - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind | VarRef _ -> assert false let add_decl_deps = decl_iter_references add_ref add_ref add_ref let add_spec_deps = spec_iter_references add_ref add_ref add_ref @@ -280,7 +284,7 @@ let rec extract_sfb env mp all = function let ms = extract_sfb env mp all msb in let kn = make_kn mp empty_dirpath l in let mind = mind_of_kn kn in - let b = Visit.needed_kn mind in + let b = Visit.needed_ind mind in if all || b then let d = Dind (kn, extract_inductive env mind) in if (not b) && (logical_decl d) then ms diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 057057d1..b615955f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*) (*i*) open Util @@ -817,6 +817,18 @@ let rec decomp_lams_eta_n n m env c t = let eta_args = List.rev_map mkRel (interval 1 d) in rels, applist (lift d c,eta_args) +(* Let's try to identify some situation where extracted code + will allow generalisation of type variables *) + +let rec gentypvar_ok c = match kind_of_term c with + | Lambda _ | Const _ -> true + | App (c,v) -> + (* if all arguments are variables, these variables will + disappear after extraction (see [empty_s] below) *) + array_for_all isRel v && gentypvar_ok c + | Cast (c,_,_) -> gentypvar_ok c + | _ -> false + (*s From a constant to a ML declaration. *) let extract_std_constant env kn body typ = @@ -846,6 +858,17 @@ let extract_std_constant env kn body typ = then decompose_lam_n m body else decomp_lams_eta_n n m env body typ in + (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) + let rels, c = + let n = List.length rels in + let s,s' = list_split_at n s in + let k = sign_kind s in + let empty_s = (k = EmptySig || k = SafeLogicalSig) in + if lang () = Ocaml && empty_s && not (gentypvar_ok c) + && s' <> [] && type_maxvar t <> 0 + then decomp_lams_eta_n (n+1) n env body typ + else rels,c + in let n = List.length rels in let s = list_firstn n s in let l,l' = list_split_at n l in diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 57b7c365..29d3da4d 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i*) (*s Production of Haskell syntax. *) @@ -297,7 +297,7 @@ let pp_decl = function try let ids,s = find_type_custom r in prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s - with not_found -> + with Not_found -> prlist (fun id -> pr_id id ++ str " ") l ++ if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n" else str "=" ++ spc () ++ pp_type false l t diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 745a78fe..a079aacc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) (*i*) open Pp @@ -656,10 +656,10 @@ let rec tmp_head_lams = function let rec ast_glob_subst s t = match t with | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in - (try linear_beta_red a (Refmap.find refe s) + (try linear_beta_red a (Refmap'.find refe s) with Not_found -> MLapp (f, a)) | MLglob ((ConstRef kn) as refe) -> - (try Refmap.find refe s with Not_found -> t) + (try Refmap'.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -1259,7 +1259,7 @@ let con_of_string s = | [] -> assert false let manual_inline_set = - List.fold_right (fun x -> Cset.add (con_of_string x)) + List.fold_right (fun x -> Cset_env.add (con_of_string x)) [ "Coq.Init.Wf.well_founded_induction_type"; "Coq.Init.Wf.well_founded_induction"; "Coq.Init.Wf.Acc_iter"; @@ -1271,10 +1271,10 @@ let manual_inline_set = "Coq.Init.Logic.eq_rect_r"; "Coq.Init.Specif.proj1_sig"; ] - Cset.empty + Cset_env.empty let manual_inline = function - | ConstRef c -> Cset.mem c manual_inline_set + | ConstRef c -> Cset_env.mem c manual_inline_set | _ -> false (* If the user doesn't say he wants to keep [t], we inline in two cases: diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index d6b85f12..d2ac48ea 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i*) open Util open Names open Term open Libnames open Miniml +open Table (*s Utility functions over ML types with meta. *) @@ -108,7 +109,7 @@ val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast -val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast +val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 15145344..b4334750 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) open Names open Declarations @@ -217,45 +217,25 @@ let get_decl_in_structure r struc = let dfix_to_mlfix rv av i = let rec make_subst n s = if n < 0 then s - else make_subst (n-1) (Refmap.add rv.(n) (n+1) s) + else make_subst (n-1) (Refmap'.add rv.(n) (n+1) s) in - let s = make_subst (Array.length rv - 1) Refmap.empty + let s = make_subst (Array.length rv - 1) Refmap'.empty in let rec subst n t = match t with | MLglob ((ConstRef kn) as refe) -> - (try MLrel (n + (Refmap.find refe s)) with Not_found -> t) + (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) -let rec optim to_appear s = function - | [] -> [] - | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l -> - if List.mem r to_appear - then d :: (optim to_appear s l) - else optim to_appear s l - | Dterm (r,t,typ) :: l -> - let t = normalize (ast_glob_subst !s t) in - let i = inline r t in - if i then s := Refmap.add r t !s; - if not i || modular () || List.mem r to_appear - then - let d = match optimize_fix t with - | MLfix (0, _, [|c|]) -> - Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|]) - | t -> Dterm (r, t, typ) - in d :: (optim to_appear s l) - else optim to_appear s l - | d :: l -> d :: (optim to_appear s l) - let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in - if i then s := Refmap.add r a !s; + if i then s := Refmap'.add r a !s; if top && i && not (modular ()) && not (List.mem r to_appear) then optim_se top to_appear s lse else @@ -271,7 +251,7 @@ let rec optim_se top to_appear s = function let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body - then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s + then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; if !all && top && not (modular ()) @@ -302,11 +282,11 @@ let base_r = function | _ -> assert false let reset_needed, add_needed, found_needed, is_needed = - let needed = ref Refset.empty in - ((fun l -> needed := Refset.empty), - (fun r -> needed := Refset.add (base_r r) !needed), - (fun r -> needed := Refset.remove (base_r r) !needed), - (fun r -> Refset.mem (base_r r) !needed)) + let needed = ref Refset'.empty in + ((fun l -> needed := Refset'.empty), + (fun r -> needed := Refset'.add (base_r r) !needed), + (fun r -> needed := Refset'.remove (base_r r) !needed), + (fun r -> Refset'.mem (base_r r) !needed)) let declared_refs = function | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|] @@ -361,7 +341,7 @@ let check_implicits = function | _ -> false let optimize_struct to_appear struc = - let subst = ref (Refmap.empty : ml_ast Refmap.t) in + let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in let opt_struc = List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index fd640388..a7e636ff 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) open Names open Term @@ -21,6 +21,13 @@ open Util open Pp open Miniml +(** Sets and maps for [global_reference] that do _not_ work modulo + name equivalence (otherwise use Refset / Refmap ) *) + +module RefOrd = struct type t = global_reference let compare = compare end +module Refmap' = Map.Make(RefOrd) +module Refset' = Set.Make(RefOrd) + (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) let occur_kn_in_ref kn = function @@ -119,37 +126,47 @@ let rec add_labels_mp mp = function (*s Constants tables. *) -let terms = ref (Cmap.empty : ml_decl Cmap.t) -let init_terms () = terms := Cmap.empty -let add_term kn d = terms := Cmap.add kn d !terms -let lookup_term kn = Cmap.find kn !terms +let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t) +let init_terms () = terms := Cmap_env.empty +let add_term kn d = terms := Cmap_env.add kn d !terms +let lookup_term kn = Cmap_env.find kn !terms -let types = ref (Cmap.empty : ml_schema Cmap.t) -let init_types () = types := Cmap.empty -let add_type kn s = types := Cmap.add kn s !types -let lookup_type kn = Cmap.find kn !types +let types = ref (Cmap_env.empty : ml_schema Cmap_env.t) +let init_types () = types := Cmap_env.empty +let add_type kn s = types := Cmap_env.add kn s !types +let lookup_type kn = Cmap_env.find kn !types (*s Inductives table. *) -let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t) -let init_inductives () = inductives := Mindmap.empty -let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives -let lookup_ind kn = Mindmap.find kn !inductives +let inductives = + ref (Mindmap_env.empty : (mutual_inductive_body * ml_ind) Mindmap_env.t) +let init_inductives () = inductives := Mindmap_env.empty +let add_ind kn mib ml_ind = + inductives := Mindmap_env.add kn (mib,ml_ind) !inductives +let lookup_ind kn = Mindmap_env.find kn !inductives (*s Recursors table. *) +(* NB: here we can use the equivalence between canonical + and user constant names : Cset is fine, no need for [Cset_env] *) + let recursors = ref Cset.empty let init_recursors () = recursors := Cset.empty let add_recursors env kn = - let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in + let mk_con id = + make_con_equiv + (modpath (user_mind kn)) + (modpath (canonical_mind kn)) + empty_dirpath (label_of_id id) + in let mib = Environ.lookup_mind kn env in Array.iter (fun mip -> let id = mip.mind_typename in - let kn_rec = make_kn (Nameops.add_suffix id "_rec") - and kn_rect = make_kn (Nameops.add_suffix id "_rect") in - recursors := Cset.add kn_rec (Cset.add kn_rect !recursors)) + let c_rec = mk_con (Nameops.add_suffix id "_rec") + and c_rect = mk_con (Nameops.add_suffix id "_rect") in + recursors := Cset.add c_rec (Cset.add c_rect !recursors)) mib.mind_packets let is_recursor = function @@ -158,6 +175,8 @@ let is_recursor = function (*s Record tables. *) +(* NB: here, working modulo name equivalence is ok *) + let projs = ref (Refmap.empty : int Refmap.t) let init_projs () = projs := Refmap.empty let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs @@ -166,12 +185,12 @@ let projection_arity r = Refmap.find r !projs (*s Table of used axioms *) -let info_axioms = ref Refset.empty -let log_axioms = ref Refset.empty -let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty -let add_info_axiom r = info_axioms := Refset.add r !info_axioms -let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms -let add_log_axiom r = log_axioms := Refset.add r !log_axioms +let info_axioms = ref Refset'.empty +let log_axioms = ref Refset'.empty +let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty +let add_info_axiom r = info_axioms := Refset'.add r !info_axioms +let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms +let add_log_axiom r = log_axioms := Refset'.add r !log_axioms (*s Extraction mode: modular or monolithic *) @@ -220,7 +239,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) let err s = errorlabstrm "Extraction" s let warning_axioms () = - let info_axioms = Refset.elements !info_axioms in + let info_axioms = Refset'.elements !info_axioms in if info_axioms = [] then () else begin let s = if List.length info_axioms = 1 then "axiom" else "axioms" in @@ -229,7 +248,7 @@ let warning_axioms () = ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) ++ str "." ++ fnl ()) end; - let log_axioms = Refset.elements !log_axioms in + let log_axioms = Refset'.elements !log_axioms in if log_axioms = [] then () else begin let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" @@ -457,16 +476,16 @@ let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) (*s Extraction Inline/NoInline *) -let empty_inline_table = (Refset.empty,Refset.empty) +let empty_inline_table = (Refset'.empty,Refset'.empty) let inline_table = ref empty_inline_table -let to_inline r = Refset.mem r (fst !inline_table) +let to_inline r = Refset'.mem r (fst !inline_table) -let to_keep r = Refset.mem r (snd !inline_table) +let to_keep r = Refset'.mem r (snd !inline_table) let add_inline_entries b l = - let f b = if b then Refset.add else Refset.remove in + let f b = if b then Refset'.add else Refset'.remove in let i,k = !inline_table in inline_table := (List.fold_right (f b) l i), @@ -504,14 +523,14 @@ let extraction_inline b l = let print_extraction_inline () = let (i,n)= !inline_table in - let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in + let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in msg (str "Extraction Inline:" ++ fnl () ++ - Refset.fold + Refset'.fold (fun r p -> (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++ str "Extraction NoInline:" ++ fnl () ++ - Refset.fold + Refset'.fold (fun r p -> (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ())) @@ -529,10 +548,10 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) type int_or_id = ArgInt of int | ArgId of identifier -let implicits_table = ref Refmap.empty +let implicits_table = ref Refmap'.empty let implicits_of_global r = - try Refmap.find r !implicits_table with Not_found -> [] + try Refmap'.find r !implicits_table with Not_found -> [] let add_implicits r l = let typ = Global.type_of_global r in @@ -552,7 +571,7 @@ let add_implicits r l = safe_pr_global r)) in let l' = List.map check l in - implicits_table := Refmap.add r l' !implicits_table + implicits_table := Refmap'.add r l' !implicits_table (* Registration of operations for rollback. *) @@ -568,7 +587,7 @@ let (implicit_extraction,_) = let _ = declare_summary "Extraction Implicit" { freeze_function = (fun () -> !implicits_table); unfreeze_function = ((:=) implicits_table); - init_function = (fun () -> implicits_table := Refmap.empty) } + init_function = (fun () -> implicits_table := Refmap'.empty) } (* Grammar entries. *) @@ -658,22 +677,22 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) let use_type_scheme_nb_args, register_type_scheme_nb_args = let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r -let customs = ref Refmap.empty +let customs = ref Refmap'.empty -let add_custom r ids s = customs := Refmap.add r (ids,s) !customs +let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs -let is_custom r = Refmap.mem r !customs +let is_custom r = Refmap'.mem r !customs let is_inline_custom r = (is_custom r) && (to_inline r) -let find_custom r = snd (Refmap.find r !customs) +let find_custom r = snd (Refmap'.find r !customs) -let find_type_custom r = Refmap.find r !customs +let find_type_custom r = Refmap'.find r !customs -let custom_matchs = ref Refmap.empty +let custom_matchs = ref Refmap'.empty let add_custom_match r s = - custom_matchs := Refmap.add r s !custom_matchs + custom_matchs := Refmap'.add r s !custom_matchs let indref_of_match pv = if Array.length pv = 0 then raise Not_found; @@ -682,11 +701,11 @@ let indref_of_match pv = | _ -> raise Not_found let is_custom_match pv = - try Refmap.mem (indref_of_match pv) !custom_matchs + try Refmap'.mem (indref_of_match pv) !custom_matchs with Not_found -> false let find_custom_match pv = - Refmap.find (indref_of_match pv) !custom_matchs + Refmap'.find (indref_of_match pv) !custom_matchs (* Registration of operations for rollback. *) @@ -703,7 +722,7 @@ let (in_customs,_) = let _ = declare_summary "ML extractions" { freeze_function = (fun () -> !customs); unfreeze_function = ((:=) customs); - init_function = (fun () -> customs := Refmap.empty) } + init_function = (fun () -> customs := Refmap'.empty) } let (in_custom_matchs,_) = declare_object @@ -717,7 +736,7 @@ let (in_custom_matchs,_) = let _ = declare_summary "ML extractions custom match" { freeze_function = (fun () -> !custom_matchs); unfreeze_function = ((:=) custom_matchs); - init_function = (fun () -> custom_matchs := Refmap.empty) } + init_function = (fun () -> custom_matchs := Refmap'.empty) } (* Grammar entries. *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a3199b50..ff4780a1 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i*) open Names open Libnames open Miniml open Declarations +module Refset' : Set.S with type elt = global_reference +module Refmap' : Map.S with type key = global_reference + val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index d287913d..e47f19bf 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -235,7 +235,7 @@ let warning_error names e = (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ if do_observe () then Cerrors.explain_exn e else mt ()) - | _ -> anomaly "" + | _ -> raise e VERNAC COMMAND EXTEND NewFunctionalScheme @@ -263,11 +263,11 @@ VERNAC COMMAND EXTEND NewFunctionalScheme end | _ -> assert false (* we can only have non empty list *) end - | e -> + | e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e - end + ] END (***** debug only ***) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f5a5fbd4..a61671f8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -294,7 +294,7 @@ let warning_error names e = (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) - | _ -> anomaly "" + | _ -> raise e let error_error names e = let e_explain e = @@ -308,7 +308,7 @@ let error_error names e = (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) - | _ -> anomaly "" + | _ -> raise e let generate_principle on_error is_general do_built fix_rec_l recdefs interactive_proof diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a980d963..6376d023 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1434,7 +1434,7 @@ let micromega_gen (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately this instance of Coq isn't aware of the presence of any \"csdp\" executable. \n\n" - ^ "You may need to specify the location during Coq's pre-compilation configuration step")) gl + ^ "This executable should be in PATH")) gl let lift_ratproof prover l = match prover l with diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 885f7fb6..90b409ba 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: subtac.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Global open Pp @@ -80,7 +80,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook = in let c = solve_tccs_in_type env id isevars evm c typ in Lemmas.start_proof id kind c (fun loc gr -> - Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps; + Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; hook loc gr) let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index b2bf9912..4927adbe 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*) +(*i $Id: subtac_classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*) open Pretyping open Evd @@ -123,7 +123,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p match props with | Inr term -> let c = interp_casted_constr_evars evars env' term cty in - Inr (c, subst) + Inr c | Inl props -> let get_id = function @@ -162,7 +162,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in term, termtype - | Inr (def, subst) -> + | Inr def -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in term, termtype @@ -174,7 +174,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let hook vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in let inst = Typeclasses.new_instance k pri global (ConstRef cst) in - Impargs.declare_manual_implicits false gr ~enriching:false imps; + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; Typeclasses.add_instance inst in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index e7dd7ef1..a83611a4 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -333,7 +333,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || impls <> [] then - Impargs.declare_manual_implicits false gr impls + Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ @@ -341,7 +341,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let typ = it_mkProd_or_LetIn top_arity binders_rel in let hook l gr = if Impargs.is_implicit_args () || impls <> [] then - Impargs.declare_manual_implicits false gr impls + Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ in let fullcoqc = Evarutil.nf_evar !isevars def in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 1424618f..b76d0cb0 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -211,7 +211,7 @@ let declare_definition prg = in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr prg.prg_implicits; + Impargs.declare_manual_implicits false gr [prg.prg_implicits]; print_message (Subtac_utils.definition_message prg.prg_name); progmap_remove prg; prg.prg_hook local gr; diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9027315e..09603d8b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *) open Util open Names @@ -1089,12 +1089,6 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = let names = get_names pb.env cs_args eqns in let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in - let _,typs',_ = - List.fold_right - (fun (na,c,t as d) (env,typs,tms) -> - let tms = List.map List.tl tms in - (push_rel d env, (na,NotInd(c,t))::typs,tms)) - typs (pb.env,[],List.map fst eqns) in let dep_sign = find_dependencies_signature @@ -1114,9 +1108,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = let pred_is_not_dep = noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in - let typs'' = + let typs' = list_map2_i - (fun i (na,t) deps -> + (fun i d deps -> + let (na,c,t) = map_rel_declaration (lift i) d in let dep = match dep with | Name _ as na',k -> (if na <> Anonymous then na else na'),k | Anonymous,KnownNotDep -> @@ -1125,15 +1120,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = else (force_name na,KnownDep) | _,_ -> anomaly "Inconsistent dependency" in - ((mkRel i, lift_tomatch_type i t),deps,dep)) - 1 typs' (List.rev dep_sign) in + ((mkRel i, NotInd (c,t)),deps,dep)) + 1 typs (List.rev dep_sign) in let pred = - specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in - - let currents = List.map (fun x -> Pushed x) typs'' in + specialize_predicate typs' (realnames,dep) arsign const_info tomatch pb.pred in - let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in + let currents = List.map (fun x -> Pushed x) typs' in let ind = appvect ( @@ -1141,7 +1134,7 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = List.map (lift const_info.cs_nargs) const_info.cs_params), const_info.cs_concl_realargs) in - let cur_alias = lift (List.length sign) current in + let cur_alias = lift (List.length typs) current in let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in let tomatch = List.rev_append currents tomatch in @@ -1150,13 +1143,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = raise_pattern_matching_error (dummy_loc, pb.env, NonExhaustive (complete_history history)); - sign, + typs, { pb with - env = push_rels sign pb.env; + env = push_rels typs pb.env; tomatch = tomatch; pred = pred; history = history; - mat = List.map (push_rels_eqn_with_names sign) submat } + mat = List.map (push_rels_eqn_with_names typs) submat } (********************************************************************** INVARIANT: @@ -1597,7 +1590,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c = | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> (match tmtype with - NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) + NotInd _ -> (subst, len - signlen) | IsInd (_, IndType(indf,realargs),_) -> let subst = if dependent tm c && List.for_all isRel realargs @@ -1707,6 +1700,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) + let initial_pushed = List.map2 (fun tm na -> Pushed(tm,[],na)) tomatchs nal in (* A typing function that provides with a canonical term for absurd cases*) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7b4b5e07..1c17ff88 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *) open Pp open Util @@ -235,6 +235,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct str " depends on pattern variable name " ++ pr_id id ++ str " which is not bound in current context.") + let protected_get_type_of env sigma c = + try Retyping.get_type_of env sigma c + with Anomaly _ -> + errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") + let pretype_id loc env sigma (lvar,unbndltacvars) id = try let (n,_,typ) = lookup_rel_id id (rel_context env) in @@ -244,7 +249,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let (ids,c) = List.assoc id lvar in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in - { uj_val = c; uj_type = Retyping.get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let (_,_,typ) = lookup_named id env in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3d97d8b2..78626854 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,14 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*) (*i*) open Names open Nametab open Term open Libnames -open Classops open Libobject open Library (*i*) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index ada14fda..9be84e14 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqmktop.ml 13430 2010-09-18 08:15:25Z herbelin $ *) (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the @@ -233,7 +233,7 @@ let declare_loading_string () = let ppf = Format.std_formatter;; Mltop.set_top {Mltop.load_obj= - (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\"); + (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\ Mltop.use_file=Topdirs.dir_use ppf; Mltop.add_dir=Topdirs.dir_directory; Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" diff --git a/tactics/auto.ml b/tactics/auto.ml index faf0482b..ca2f4916 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: auto.ml 13390 2010-09-02 08:03:01Z herbelin $ *) open Pp open Util @@ -706,12 +706,11 @@ let print_applicable_hint () = (* displays the whole hint database db *) let print_hint_db db = let (ids, csts) = Hint_db.transparent_state db in - msg (hov 0 + msgnl (hov 0 ((if Hint_db.use_dn db then str"Discriminated database" - else str"Non-discriminated database") ++ fnl ())); - msg (hov 0 - (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++ - str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); + else str"Non-discriminated database"))); + msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids)); + msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts)); Hint_db.iter (fun head hintlist -> match head with diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 3e2191d1..825ec492 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: evar_tactics.ml 13428 2010-09-17 18:03:40Z herbelin $ *) open Term open Util @@ -53,7 +53,8 @@ let instantiate n (ist,rawc) ido gl = gl let let_evar name typ gls = - let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) typ in + let src = (dummy_loc,GoalEvar) in + let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None nowhere) gls diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e1ac42c2..3f069ab2 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *) open Pp open Pcoq @@ -624,3 +624,8 @@ TACTIC EXTEND hget_evar END (**********************************************************************) + +TACTIC EXTEND constr_eq +| [ "constr_eq" constr(x) constr(y) ] -> [ + if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ] +END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 9d99ad96..d8497a7d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -431,29 +431,30 @@ let pointwise_or_dep_relation n t car rel = [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]) let lift_cstr env sigma evars (args : constr list) ty cstr = - let cstr = - let start env car = - match cstr with - | None | Some (_, None) -> - Evarutil.e_new_evar evars env (mk_relation car) - | Some (ty, Some rel) -> rel - in - let rec aux env prod n = - if n = 0 then start env prod - else - match kind_of_term (Reduction.whd_betadeltaiota env prod) with - | Prod (na, ty, b) -> - if noccurn 1 b then - let b' = lift (-1) b in - let rb = aux env b' (pred n) in - mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |]) - else - let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in - mkApp (Lazy.force forall_relation, - [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]) - | _ -> assert false - in aux env ty (List.length args) - in Some (ty, cstr) + let start env car = + match cstr with + | None | Some (_, None) -> + Evarutil.e_new_evar evars env (mk_relation car) + | Some (ty, Some rel) -> rel + in + let rec aux env prod n args = + if n = 0 then Some (start env prod) + else + match kind_of_term (Reduction.whd_betadeltaiota env prod) with + | Prod (na, ty, b) -> + if noccurn 1 b then + let b' = lift (-1) b in + let rb = aux env b' (pred n) (List.tl args) in + Option.map (fun rb -> mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])) + rb + else + let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) (List.tl args) in + Option.map + (fun rb -> mkApp (Lazy.force forall_relation, + [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])) + rb + | _ -> None + in Option.map (fun rel -> (ty, rel)) (aux env ty (List.length args) args) let unlift_cstr env sigma = function | None -> None diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 95e44c40..ba9a5173 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 13360 2010-07-30 08:47:08Z herbelin $ *) +(* $Id: tacinterp.ml 13489 2010-10-03 22:27:12Z herbelin $ *) open Constrintern open Closure @@ -401,8 +401,10 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist -> - RVar (dloc,id), None + | Ident (_,id) as r when not strict & find_hyp id ist -> + RVar (dloc,id), Some (CRef r) + | Ident (_,id) as r when find_ctxvar id ist -> + RVar (dloc,id), if strict then None else Some (CRef r) | r -> let loc,_ as lqid = qualid_of_reference r in RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) @@ -564,9 +566,10 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) - | AN (Ident (_,id)) when - (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> - ArgArg (EvalVarRef id, None) + | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist -> + ArgArg (EvalVarRef id, Some (loc,id)) + | AN (Ident (loc,id)) when find_ctxvar id ist -> + ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -1138,7 +1141,8 @@ let interp_hyp ist gl (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.") + else user_err_loc (loc,"eval_variable", + str "No such hypothesis: " ++ pr_id id ++ str ".") let hyp_list_of_VList env = function | VList l -> List.map (coerce_to_hyp env) l @@ -1210,7 +1214,7 @@ let interp_evaluable ist env = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> Pretype_errors.error_var_not_found_loc loc id) + | _ -> error_global_not_found_loc (loc,qualid_of_ident id)) | ArgArg (r,None) -> r | ArgVar locid -> interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid @@ -1616,8 +1620,9 @@ let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with | ElimOnConstr c -> - let sigma, c = interp_constr_with_bindings ist env sigma c in - sigma, ElimOnConstr c + let sigma', (c,b) = interp_constr_with_bindings ist env sigma c in + let sigma, c = solve_remaining_evars false true env sigma sigma' c in + sigma, ElimOnConstr (c,b) | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9e4be0af..4ecc4739 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *) open Pp open Util @@ -868,13 +868,18 @@ type conjunction_status = | DefinedRecord of constant option list | NotADefinedRecordUseScheme of constr -let make_projection params cstr sign elim i n c = +let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in - if noccur_between 1 (n-i-1) t then + if + (* excludes dependent projection types *) + noccur_between 1 (n-i-1) t + (* excludes flexible projection types *) + && not (isEvar (fst (whd_betaiota_stack sigma t))) + then let t = lift (i+1-n) t in Some (beta_applist (elim,params@[t;branch]),t) else @@ -883,7 +888,8 @@ let make_projection params cstr sign elim i n c = match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in - Some (beta_applist (mkConst proj,params),prod_applist t (params@[c])) + let args = extended_rel_vect 0 sign in + Some (beta_applist (mkConst proj,params),prod_applist t (params@[mkApp (c,args)])) | None -> None in Option.map (fun (abselim,elimt) -> let c = beta_applist (abselim,[mkApp (c,extended_rel_vect 0 sign)]) in @@ -908,7 +914,7 @@ let descend_in_conjunctions tac exit c gl = NotADefinedRecordUseScheme elim in tclFIRST (list_tabulate (fun i gl -> - match make_projection params cstr sign elim i n c with + match make_projection (project gl) params cstr sign elim i n c with | None -> tclFAIL 0 (mt()) gl | Some (p,pt) -> tclTHENS @@ -2188,6 +2194,8 @@ let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl) let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq") let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl") +let coq_block = lazy (Coqlib.coq_constant "tactics" ["Program";"Equality"] "block") + let mkEq t x y = mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |]) @@ -2303,23 +2311,6 @@ let hyps_of_vars env sign nogen hyps = sign in lh -exception Seen - -let linear vars args = - let seen = ref vars in - try - Array.iter (fun i -> - let rels = ids_of_constr ~all:true Idset.empty i in - let seen' = - Idset.fold (fun id acc -> - if Idset.mem id acc then raise Seen - else Idset.add id acc) - rels !seen - in seen := seen') - args; - true - with Seen -> false - let is_defined_variable env id = pi2 (lookup_named id env) <> None @@ -2373,19 +2364,23 @@ let abstract_args gl generalize_vars dep id defined f args = nongenvars, Idset.union argvars vars, env) in let f', args' = decompose_indapp f args in + let parvars = ids_of_constr ~all:true Idset.empty f' in let dogen, f', args' = - let parvars = ids_of_constr ~all:true Idset.empty f' in - if not (linear parvars args') then true, f, args - else - match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with - | None -> false, f', args' - | Some nonvar -> - let before, after = array_chop nonvar args' in - true, mkApp (f', before), after + let seen = ref parvars in + let find i x = not (isVar x) || + let v = destVar x in + if is_defined_variable env v || Idset.mem v !seen then true + else (seen := Idset.add v !seen; false) + in + match array_find_i find args' with + | None -> false, f', args' + | Some nonvar -> + let before, after = array_chop nonvar args' in + true, mkApp (f', before), after in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,Idset.empty,env) args' + Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -2440,14 +2435,14 @@ let specialize_eqs id gl = match kind_of_term ty with | Prod (na, t, b) -> (match kind_of_term t with - | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) -> + | App (eq, [| eqty; x; y |]) when in_eqs && eq_constr eq (Lazy.force coq_eq) -> let c = if noccur_between 1 (List.length ctx) x then y else x in let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) -> + | App (heq, [| eqty; x; eqty'; y |]) when in_eqs && eq_constr heq (Lazy.force coq_heq) -> let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in @@ -2459,8 +2454,10 @@ let specialize_eqs id gl = else let e = e_new_evar evars (push_rel_context ctx env) t in aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) + | App (f, args) when eq_constr f (Lazy.force coq_block) && not in_eqs -> + aux true ctx acc args.(1) | t -> acc, in_eqs, ctx, ty - in + in let acc, worked, ctx, ty = aux false [] (mkVar id) ty in let ctx' = nf_rel_context_evar !evars ctx in let ctx'' = List.map (fun (n,b,t as decl) -> diff --git a/test-suite/Makefile b/test-suite/Makefile index 2503368f..62d443d0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ endif command := $(coqtop) -top Top -load-vernac-source coqc := $(coqtop) -compile +coqdep := $(BIN)coqdep SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) @@ -74,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) xml bugs +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ####################################################################### # Phony targets @@ -114,7 +115,6 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) # Summary ####################################################################### -summary_one = echo $(1); if [ -f $(2).log ]; then tail -n1 $(2).log; fi | sort -g summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g .PHONY: summary summary.log @@ -128,7 +128,7 @@ summary: $(call summary_dir, "Output tests", output); \ $(call summary_dir, "Interactive tests", interactive); \ $(call summary_dir, "Micromega tests", micromega); \ - $(call summary_one, "Miscellaneous tests", xml); \ + $(call summary_dir, "Miscellaneous tests", misc); \ $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ @@ -354,10 +354,12 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik. # Miscellaneous tests ####################################################################### +misc: misc/xml.log misc/deps-order.log + # Test xml compilation -xml: xml.log -xml.log: - @echo "TEST xml" +xml: misc/xml.log +misc/xml.log: + @echo "TEST misc/xml" $(HIDE){ \ echo $(call log_intro,xml); \ rm -rf misc/xml; \ @@ -365,9 +367,36 @@ xml.log: $(bincoqc) -xml misc/berardi_test 2>&1; times; \ if [ ! -d misc/xml ]; then \ echo $(log_failure); \ - echo " xml... failed"; \ + echo " misc/xml... failed"; \ else \ echo $(log_success); \ - echo " xml...apparently ok"; \ + echo " misc/xml...apparently ok"; \ fi; rm -r misc/xml; \ } > "$@" + +# Check that both coqdep and coqtop/coqc takes the later -I/-R +# Check that both coqdep and coqtop/coqc supports both -R and -I dir -as lib +# See bugs 2242, 2337, 2339 +deps-order: misc/deps-order.log +misc/deps-order.log: + @echo "TEST misc/deps-order" + $(HIDE){ \ + echo $(call log_intro,deps-order); \ + rm -f misc/deps/*/*.vo; \ + tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ + | head -n 1 > $$tmpoutput; \ + diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \ + $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \ + $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ + $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ + S=$$?; times; \ + if [ $$R = 0 -a $$S = 0 ]; then \ + echo $(log_success); \ + echo " misc/deps-order...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/deps-order...Error! (unexpected order)"; \ + fi; \ + rm $$tmpoutput; \ + } > "$@" diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v new file mode 100644 index 00000000..4ae97c97 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -0,0 +1,13 @@ +(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) +Definition interp (etyp : nat -> Type) (p: nat) := etyp p. + +Record Value (etyp : nat -> Type) := Mk { + typ : nat; + value : interp etyp typ +}. + +Definition some_value (etyp : nat -> Type) : (Value etyp). +Proof. + intros. + Fail apply Mk. (* Check that it does not raise an anomaly *) + diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v new file mode 100644 index 00000000..c17c426c --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2375.v @@ -0,0 +1,18 @@ +(* In the following code, the (superfluous) lemma [lem] is responsible +for the failure of congruence. *) + +Definition f : nat -> Prop := fun x => True. + +Lemma lem : forall x, (True -> True) = ( True -> f x). +Proof. + intros. reflexivity. +Qed. + +Goal forall (x:nat), x = x. +Proof. + intros. + assert (lem := lem). + (*clear ax.*) + congruence. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v new file mode 100644 index 00000000..c7926711 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2388.v @@ -0,0 +1,10 @@ +(* Error message was not printed in the correct environment *) + +Fail Parameters (A:Prop) (a:A A). + +(* This is a variant (reported as part of bug #2347) *) + +Require Import EquivDec. +Fail Program Instance bool_eq_eqdec : EqDec bool eq := + {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. + diff --git a/test-suite/failure/prop-set-proof-irrelevance.v b/test-suite/failure/prop-set-proof-irrelevance.v new file mode 100644 index 00000000..ad494108 --- /dev/null +++ b/test-suite/failure/prop-set-proof-irrelevance.v @@ -0,0 +1,12 @@ +Require Import ProofIrrelevance. + +Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. + exact proof_irrelevance. +Qed. + +Lemma paradox : False. + assert (H : 0 <> 1) by discriminate. + apply H. + Fail apply proof_irrelevance. (* inlined version is rejected *) + apply proof_irrelevance_set. +Qed. diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v new file mode 100644 index 00000000..62969418 --- /dev/null +++ b/test-suite/misc/deps/client/bar.v @@ -0,0 +1,11 @@ +(* We assume the file compiled with -R ../lib lib -R . client *) +(* foo alone should refer to client.foo because -R . client comes last *) + +Require Import foo. +Goal a = 1. +reflexivity. +Qed. +Require Import lib.foo. +Goal a = 0. +reflexivity. +Qed. diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v new file mode 100644 index 00000000..fc82069e --- /dev/null +++ b/test-suite/misc/deps/client/foo.v @@ -0,0 +1 @@ +Definition a := 1. diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out new file mode 100644 index 00000000..68b48d60 --- /dev/null +++ b/test-suite/misc/deps/deps.out @@ -0,0 +1 @@ +misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v new file mode 100644 index 00000000..b745fbd4 --- /dev/null +++ b/test-suite/misc/deps/lib/foo.v @@ -0,0 +1 @@ +Definition a := 0. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 59e1a935..ce3e692f 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -86,3 +86,24 @@ Fixpoint plus n m {struct n} := | 0 => m | S p => S (plus p m) end. + +(* Check multiple implicit arguments signatures *) + +Implicit Arguments eq_refl [[A] [x]] [[A]]. + +Check eq_refl : 0 = 0. + +(* Check that notations preserve implicit (since 8.3) *) + +Parameter p : forall A, A -> forall n, n = 0 -> True. +Implicit Arguments p [A n]. +Notation Q := (p 0). +Check Q eq_refl. + +(* Check implicits with Context *) + +Section C. +Context {A:Set}. +Definition h (a:A) := a. +End C. +Check h 0. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index dfa41c82..02618c2c 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -243,3 +243,35 @@ test_open_match (forall z y, y + z = 0). reflexivity. apply I. Qed. + +(* Test regular failure when clear/intro breaks soundness of the + interpretation of terms in current environment *) + +Ltac g y := clear y; assert (y=y). +Goal forall x:nat, True. +intro x. +Fail g x. +Abort. + +Ltac h y := assert (y=y). +Goal forall x:nat, True. +intro x. +Fail clear x; f x. +Abort. + +(* Do not consider evars as unification holes in Ltac matching (and at + least not as holes unrelated to the original evars) + [Example adapted from Ynot code] + *) + +Ltac not_eq e1 e2 := + match e1 with + | e2 => fail 1 + | _ => idtac + end. + +Goal True. +evar(foo:nat). +let evval := eval compute in foo in not_eq evval 1. +let evval := eval compute in foo in not_eq 1 evval. +Abort. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 47ca0836..5649e2f7 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -13,3 +13,11 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. + +(* Check regular failure when statically existing ref does not exist + any longer at run time *) + +Goal let x := 0 in True. +intro x. +Fail (clear x; unfold x). +Abort. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1aad3cec..2bfebfd8 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -15,7 +15,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff. (** Leibniz equality. *) -Program Instance eq_Reflexive : Reflexive (@eq A). -Program Instance eq_Symmetric : Symmetric (@eq A). -Program Instance eq_Transitive : Transitive (@eq A). +Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A. +Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A. +Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. (** Various combinations of reflexivity, symmetry and transitivity. *) diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 7b64ded7..cf0449f8 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,7 +8,7 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *) +(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *) (** * FMapAVL *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index be7becda..c8c5e3d6 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ i*) (** * This module proves the validity of - well-founded recursion (also known as course of values) @@ -36,6 +36,8 @@ Section Well_founded. destruct 1; trivial. Defined. + Global Implicit Arguments Acc_inv [x y] [x]. + (** A relation is well-founded if every element is accessible *) Definition well_founded := forall a:A, Acc a. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2764d1b4..53e12723 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13359 2010-07-30 08:46:55Z herbelin $ i*) +(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -33,7 +33,8 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. -Ltac unblock_goal := unfold block in *. +Ltac unblock_goal := unfold block at 1. +Ltac unblock_all := unfold block in *. (** Notation for heterogenous equality. *) @@ -41,8 +42,8 @@ Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). (** Notation for the single element of [x = x] and [x ~= x]. *) -Implicit Arguments eq_refl [[A] [x]]. -Implicit Arguments JMeq_refl [[A] [x]]. +Implicit Arguments eq_refl [[A] [x]] [A]. +Implicit Arguments JMeq_refl [[A] [x]] [A]. (** Do something on an heterogeneous equality appearing in the context. *) @@ -224,7 +225,7 @@ Ltac simplify_eqs := Ltac simplify_IH_hyps := repeat match goal with - | [ hyp : _ |- _ ] => specialize_eqs hyp + | [ hyp : context [ block _ ] |- _ ] => specialize_eqs hyp ; unfold block in hyp end. (** We split substitution tactics in the two directions depending on which @@ -389,18 +390,18 @@ Tactic Notation "intro_block_id" ident(H) := (is_introduced H ; block_goal ; revert_until H) || (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal). -Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. +Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_all. Ltac do_intros H := (try intros until H) ; (intro_block_id H || intro_block H). -Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H. +Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; block_goal ; tac H ; unblock_goal. Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim. Ltac do_depind tac H := - (try intros until H) ; intro_block H ; - generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal. + do_intros H ; generalize_eqs_vars H ; block_goal ; tac H ; + unblock_goal ; simplify_dep_elim ; simplify_IH_hyps ; unblock_all. (** To dependent elimination on some hyp. *) @@ -417,8 +418,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id. (** A variant where generalized variables should be given by the user. *) Ltac do_depelim' tac H := - (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; - simplify_IH_hyps ; unblock_goal. + (try intros until H) ; block_goal ; generalize_eqs H ; block_goal ; tac H ; unblock_goal ; + simplify_dep_elim ; simplify_IH_hyps ; unblock_all. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 0e6b2909..2f89ff53 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Syntax.v 13492 2010-10-04 21:20:01Z herbelin $ *) (** Custom notations and implicits for Coq prelude definitions. @@ -20,16 +20,14 @@ Notation " () " := tt. (** Set maximally inserted implicit arguments for standard definitions. *) -Implicit Arguments eq [[A]]. - Implicit Arguments Some [[A]]. Implicit Arguments None [[A]]. -Implicit Arguments inl [[A] [B]]. -Implicit Arguments inr [[A] [B]]. +Implicit Arguments inl [[A] [B]] [A]. +Implicit Arguments inr [[A] [B]] [B]. -Implicit Arguments left [[A] [B]]. -Implicit Arguments right [[A] [B]]. +Implicit Arguments left [[A] [B]] [A]. +Implicit Arguments right [[A] [B]] [B]. Implicit Arguments pair [[A] [B]]. Implicit Arguments fst [[A] [B]]. @@ -50,8 +48,8 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Require Import Bvector. -Implicit Arguments Vnil [[A]]. -Implicit Arguments Vcons [[A] [n]]. +Implicit Arguments Vnil [[A]] []. +Implicit Arguments Vcons [[A] [n]] []. (** Treating n-ary exists *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 4159f436..4ca49c41 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -16,8 +16,6 @@ Require Import ProofIrrelevance. Open Local Scope program_scope. -Implicit Arguments Acc_inv [A R x y]. - Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index d205c0e0..382511d9 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: Equalities.v 12662 2010-01-13 16:53:01Z letouzey $ *) +(* $Id: Equalities.v 13475 2010-09-29 14:33:13Z letouzey $ *) Require Export RelationClasses. @@ -176,8 +176,7 @@ Module Type UsualEq <: Eq := Typ <+ HasUsualEq. Module Type UsualIsEq (E:UsualEq) <: IsEq E. (* No Instance syntax to avoid saturating the Equivalence tables *) - Lemma eq_equiv : Equivalence E.eq. - Proof. exact eq_equivalence. Qed. + Definition eq_equiv : Equivalence E.eq := eq_equivalence. End UsualIsEq. Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E. diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c4e8b23c..0961e398 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -138,7 +138,7 @@ let warning_clash file dir = let d2 = Filename.dirname f2 in let dl = List.map Filename.dirname (List.rev fl) in eprintf - "*** Warning: in file %s, \n required library %s is ambiguous!\n (found %s.v in " + "*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in " file (String.concat "." dir) f; List.iter (fun s -> eprintf "%s, " s) dl; eprintf "%s and %s; used the latter)\n" d2 d1 diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d24093ff..a23a4f74 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mll 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*) (*s Utility functions for the scanners *) @@ -326,6 +326,7 @@ let def_token = | "CoInductive" | "Equations" | "Instance" + | "Declare" space+ "Instance" | "Global" space+ "Instance" let decl_token = diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0b3718ab..cbebbd79 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: output.ml 13541 2010-10-13 19:53:29Z notin $ i*) open Cdglobals open Index @@ -477,8 +477,6 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; if !header_trailer then if !footer_file_spec then let cin = Pervasives.open_in !footer_file in @@ -490,6 +488,8 @@ module Html = struct with End_of_file -> Pervasives.close_in cin else begin + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; printf "<hr/>This page has been generated by "; printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; printf "</div>\n\n</div>\n\n</body>\n</html>" diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 5828f12d..db2f9ae9 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *) open Pp open Util @@ -28,6 +28,8 @@ let guill s = "\""^s^"\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) +exception EvaluatedError of std_ppcmds * exn option + (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) let rec explain_exn_default_aux anomaly_string report_fn = function @@ -69,54 +71,6 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") - | Univ.UniverseInconsistency (o,u,v) -> - let msg = - if !Constrextern.print_universes then - spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ - str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") - ++ spc() ++ Univ.pr_uni v ++ str")" - else - mt() in - hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") - | TypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) - | PretypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) - | Typeclasses_errors.TypeClassError(env, te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te) - | InductiveError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) - | RecursionSchemeError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) - | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> - explain_exn_default_aux anomaly_string report_fn exc - | Proof_type.LtacLocated (s,exc) -> - hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () - ++ explain_exn_default_aux anomaly_string report_fn exc) - | Cases.PatternMatchingError (env,e) -> - hov 0 - (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) - | Tacred.ReductionTacticError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) - | Nametab.GlobalizationError q -> - hov 0 (str "Error:" ++ spc () ++ - str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") - | Nametab.GlobalizationConstantError q -> - hov 0 (str "Error:" ++ spc () ++ - str "No constant of this name:" ++ spc () ++ - Libnames.pr_qualid q ++ str ".") - | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure" ++ - (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ - if i=0 then str "." else str " (level " ++ int i ++ str").") - | Stdpp.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn_default_aux anomaly_string report_fn exc) | Lexer.Error Illegal_character -> hov 0 (str "Syntax error: Illegal character.") | Lexer.Error Unterminated_comment -> @@ -140,12 +94,69 @@ let rec explain_exn_default_aux anomaly_string report_fn = function else (mt ())) ++ report_fn ()) - | AlreadyDeclared msg -> - hov 0 (msg ++ str ".") + | EvaluatedError (msg,None) -> + msg + | EvaluatedError (msg,Some reraise) -> + msg ++ explain_exn_default_aux anomaly_string report_fn reraise | reraise -> hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise) ++ report_fn ()) +let wrap_vernac_error strm = + EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) + +let rec process_vernac_interp_error = function + | Univ.UniverseInconsistency (o,u,v) -> + let msg = + if !Constrextern.print_universes then + spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ + str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") + ++ spc() ++ Univ.pr_uni v ++ str")" + else + mt() in + wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") + | TypeError(ctx,te) -> + wrap_vernac_error (Himsg.explain_type_error ctx te) + | PretypeError(ctx,te) -> + wrap_vernac_error (Himsg.explain_pretype_error ctx te) + | Typeclasses_errors.TypeClassError(env, te) -> + wrap_vernac_error (Himsg.explain_typeclass_error env te) + | InductiveError e -> + wrap_vernac_error (Himsg.explain_inductive_error e) + | RecursionSchemeError e -> + wrap_vernac_error (Himsg.explain_recursion_scheme_error e) + | Cases.PatternMatchingError (env,e) -> + wrap_vernac_error (Himsg.explain_pattern_matching_error env e) + | Tacred.ReductionTacticError e -> + wrap_vernac_error (Himsg.explain_reduction_tactic_error e) + | Logic.RefinerError e -> + wrap_vernac_error (Himsg.explain_refiner_error e) + | Nametab.GlobalizationError q -> + wrap_vernac_error + (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment.") + | Nametab.GlobalizationConstantError q -> + wrap_vernac_error + (str "No constant of this name:" ++ spc () ++ + Libnames.pr_qualid q ++ str ".") + | Refiner.FailError (i,s) -> + EvaluatedError (hov 0 (str "Error: Tactic failure" ++ + (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ + if i=0 then str "." else str " (level " ++ int i ++ str")."), + None) + | AlreadyDeclared msg -> + wrap_vernac_error (msg ++ str ".") + | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> + process_vernac_interp_error exc + | Proof_type.LtacLocated (s,exc) -> + EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), + Some (process_vernac_interp_error exc)) + | Stdpp.Exc_located (loc,exc) -> + Stdpp.Exc_located (loc,process_vernac_interp_error exc) + | exc -> + exc + let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 00316007..31e0e04f 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cerrors.mli 13431 2010-09-18 08:15:29Z herbelin $ i*) (*i*) open Pp @@ -19,10 +19,14 @@ val print_loc : loc -> std_ppcmds val explain_exn : exn -> std_ppcmds -(** Same, but will re-raise all anomalies instead of explaining them *) +(** Precompute errors raised during vernac interpretation *) val explain_exn_no_anomaly : exn -> std_ppcmds +(** Pre-explain a vernac interpretation error *) + +val process_vernac_interp_error : exn -> exn + (** For debugging purpose (?), the explain function can be twicked *) val explain_exn_function : (exn -> std_ppcmds) ref diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 435ddb4d..2d8aabfc 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*) (*i*) open Names @@ -233,7 +233,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if rest <> [] then unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else - Inl (type_ctx_instance evars env' k.cl_props props subst) + Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) in evars := Evarutil.nf_evar_map !evars; let term, termtype = diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a080442c..99ca9879 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: himsg.ml 13465 2010-09-24 22:23:07Z herbelin $ *) open Pp open Util @@ -290,6 +290,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = pr_ne_context_of (str "In environment") env ++ st ++ str "." ++ fnl () ++ (try (* May fail with unresolved globals. *) + let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with _ -> mt ()) diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 4e28ccac..c2d5f31d 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ind_tables.ml 13392 2010-09-02 12:11:15Z vsiles $ i*) (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) @@ -125,7 +125,7 @@ let define internal id c = const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Scheme) in (match internal with - | KernelSilent -> () + | KernelSilent -> () | _-> definition_message id); kn diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 29d7a12c..9031d8a3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *) +(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent @@ -123,8 +123,8 @@ let declare_beq_scheme_gen internal names kn = let alarm what internal msg = let debug = false in - (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) match internal with + | KernelVerbose | KernelSilent -> (if debug then Flags.if_verbose Pp.msg_warning @@ -172,17 +172,15 @@ let beq_scheme_msg mind = let declare_beq_scheme_with l kn = try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn -(* TODO : maybe switch to KernelVerbose to have the right behaviour *) let try_declare_beq_scheme kn = (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle proof-irrelevance; improve decidability by depending on decidability for the parameters rather than on the bl and lb properties *) - try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn + try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn let declare_beq_scheme = declare_beq_scheme_with [] (* Case analysis schemes *) -(* TODO: maybe switch to KernelVerbose *) let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in @@ -192,7 +190,7 @@ let declare_one_case_analysis_scheme ind = induction scheme, the other ones share the same code with the apropriate type *) if List.mem InType kelim then - ignore (define_individual_scheme dep KernelSilent None ind) + ignore (define_individual_scheme dep KernelVerbose None ind) (* Induction/recursion schemes *) @@ -206,7 +204,6 @@ let kinds_from_type = InProp,ind_dep_scheme_kind_from_type; InSet,rec_dep_scheme_kind_from_type] - (* TODO: maybe switch to kernel verbose *) let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in @@ -216,7 +213,7 @@ let declare_one_induction_scheme ind = list_map_filter (fun (sort,kind) -> if List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop else kinds_from_type) in - List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind)) + List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind)) elims let declare_induction_schemes kn = @@ -241,10 +238,9 @@ let declare_eq_decidability_scheme_with l kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) declare_eq_decidability_gen UserVerbose l kn -(* TODO: maybe switch to kernel verbose *) let try_declare_eq_decidability kn = try_declare_scheme (eq_dec_scheme_msg (kn,0)) - declare_eq_decidability_gen KernelSilent [] kn + declare_eq_decidability_gen KernelVerbose [] kn let declare_eq_decidability = declare_eq_decidability_scheme_with [] @@ -252,36 +248,34 @@ let ignore_error f x = try ignore (f x) with _ -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin - ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind); - ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind); + ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind); + ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind); ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind - KernelSilent None ind); + KernelVerbose None ind); (* These ones expect the equality to be symmetric; the first one also *) (* needs eq *) - ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind; + ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind; ignore_error - (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind; + (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind; ignore_error - (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind + (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind end -(* TODO: maybe switch to kernel verbose *) let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with _ -> false then - ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind) + ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else warning "Cannot build congruence scheme because eq is not found" end -(* TODO: maybe switch to kernel verbose *) let declare_sym_scheme ind = if Hipattern.is_inductive_equality ind then (* Expect the equality to be symmetric *) - ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind + ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind (* Scheme command *) diff --git a/toplevel/record.ml b/toplevel/record.ml index cd569178..773d3390 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: record.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -259,8 +259,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls mind_entry_record = true; mind_entry_finite = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in -(* TODO : maybe switch to KernelVerbose *) - let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in @@ -325,8 +324,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; Classes.set_typeclass_transparency (EvalConstRef cst) false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); cref, [proj_name, Some proj_cst] diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7f8bcb9e..a00efc5c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *) (* Parsing of vernacular. *) @@ -44,7 +44,7 @@ let raise_with_file file exc = ((b, f, loc), e) | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) - | _ -> ((false,file,cmdloc), re) + | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in raise (Error_in_file (file, inner, disable_drop inex)) @@ -198,7 +198,10 @@ let rec vernac_com interpfun (loc,com) = with e -> stop(); raise e end - | v -> if not !just_parsing then interpfun v + | v -> + if not !just_parsing then + States.with_heavy_rollback interpfun + Cerrors.process_vernac_interp_error v in try @@ -239,7 +242,7 @@ and read_vernac_file verbosely s = * backtracking. *) let raw_do_vernac po = - vernac (States.with_heavy_rollback Vernacentries.interp) (po,None); + vernac Vernacentries.interp (po,None); Lib.add_frozen_state(); Lib.mark_end_of_command() diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 254f690c..d74711c2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -172,7 +172,7 @@ let show_match id = | [] -> assert false | [x] -> "| "^ x ^ " => \n" ^ acc | x::l -> - "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" + "| " ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ " => \n" ^ acc) "end" patterns in msg (str ("match # with\n" ^ cases)) @@ -775,11 +775,11 @@ let vernac_syntactic_definition lid = Metasyntax.add_syntactic_definition (snd lid) let vernac_declare_implicits local r = function - | Some imps -> - Impargs.declare_manual_implicits local (smart_global r) ~enriching:false - (List.map (fun (ex,b,f) -> ex, (b,true,f)) imps) - | None -> + | [] -> Impargs.declare_implicits local (smart_global r) + | _::_ as imps -> + Impargs.declare_manual_implicits local (smart_global r) ~enriching:false + (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) let vernac_reserve bl = let sb_decl = (fun (idl,c) -> @@ -1113,7 +1113,7 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) - | PrintAbout qid -> msgnl (print_about qid) + | PrintAbout qid -> msg (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 5eb220cb..b5af665c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) open Util open Names @@ -313,7 +313,7 @@ type vernac_expr = | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag | VernacDeclareImplicits of locality_flag * reference or_by_notation * - (explicitation * bool * bool) list option + (explicitation * bool * bool) list list | VernacReserve of simple_binder list | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of |