diff options
103 files changed, 650 insertions, 1157 deletions
diff --git a/.bintray.json b/.bintray.json index 9bae43846f..fb9e553685 100644 --- a/.bintray.json +++ b/.bintray.json @@ -6,7 +6,7 @@ }, "version": { - "name": "8.7+alpha" + "name": "8.8+alpha" }, "files": diff --git a/.gitignore b/.gitignore index 5ee2f3f77b..36536ec964 100644 --- a/.gitignore +++ b/.gitignore @@ -86,6 +86,7 @@ test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject test-suite/coqdoc/Coqdoc.* test-suite/coqdoc/index.html +test-suite/coqdoc/coqdoc.css # documentation @@ -9,6 +9,7 @@ ## If you're mentionned here and want to update your information, ## either amend this file and commit it, or contact the coqdev list +Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> Jim Apple <github.public@jbapple.com> jbapple <github.public@jbapple.com> Bruno Barras <bruno.barras@inria.fr> barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> Bruno Barras <bruno.barras@inria.fr> barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -27,7 +28,7 @@ Judicaël Courant <courant@gforge> courant <courant@85f007b7-54 Pierre Courtieu <Pierre.Courtieu@cnam.fr> courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> David Delahaye <delahaye@gforge> delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7> -Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> ddr <ddr@85f007b7-540e-0410-9357-904b9bb8a0f7> +Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -36,7 +37,9 @@ Julien Forest <julien.forest@ensiie.fr> jforest <jforest@85f007b7-540 Julien Forest <julien.forest@ensiie.fr> forest <jforest@mourvedre.ensiie.fr> Julien Forest <julien.forest@ensiie.fr> jforest <jforest@thune> Julien Forest <julien.forest@ensiie.fr> jforest <jforest@daneel.lan.home> +Julien Forest <julien.forest@ensiie.fr> Julien Forest <forest@ensiie.fr> Emilio Jesus Gallego Arias <e+git@x80.org> Emilio Jesús Gallego Arias <e+git@x80.org> +Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> Stéphane Glondu <steph@glondu.net> glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> Stéphane Glondu <steph@glondu.net> Stephane Glondu <steph@glondu.net> Benjamin Grégoire <benjamin.gregoire@inria.fr> Benjamin Gregoire <Benjamin.Gregoire@inria.fr> @@ -51,9 +54,12 @@ Tom Hutchinson <thutchin@gforge> thutchin <thutchin@85f007b7-5 Cezary Kaliszyk <cek@gforge> cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7> Florent Kirchner <fkirchne@gforge> fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7> Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7> -Matej Kosik <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> +Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> +Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> +William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> +Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> @@ -68,15 +74,19 @@ Julien Narboux <jnarboux@gforge> jnarboux <jnarboux@85f007b7-5 Julien Narboux <jnarboux@gforge> narboux <narboux@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Marc Notin <notin@gforge> notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty <notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Marc Notin <notin@gforge> notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> -Russel O'Connor <roconnor@gforge> roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> +Russell O'Connor <roconnor@blockstream.io> roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> +Russell O'Connor <roconnor@blockstream.io> roconnor-blockstream <roconnor@blockstream.com> Christine Paulin <cpaulin@gforge> cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7> Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> -Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> +Lars Rasmusson <lars.rasmusson@sics.se> larsr <Lars.Rasmusson@sics.se> +Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> ddr <ddr@85f007b7-540e-0410-9357-904b9bb8a0f7> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@gforge> +Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> +Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> diff --git a/.travis.yml b/.travis.yml index 7a0e80b540..9300505f37 100644 --- a/.travis.yml +++ b/.travis.yml @@ -167,10 +167,19 @@ matrix: user: maximedenes file: .bintray.json key: - secure: "GDRjXPNvYHJBPMJqbXsSUAAPAZeGvr+mns80eYUD47Uxvueivql5VJ9d8MwLRJOV6lzwnQ1+F65WOKsR/JARMMRuVUKg3dAa3w1j8s2Yr/gwqsLt0G4Roqp93eTFDvs2X0xzzncN31G/NcV/5suc3oXuqjIF7EUSyrtiJUpMcIfFoMHWmdcGM9az4djIKYTzczAs+8MPSfrYD1AAqx2Ezeu+xDEmtvQ0w7OyO48ArUO4K5AWCRWdzSMN0A2s1w72fiCEfMgqzphzzJfRMPzp0rTF6/4CKRbtJpnSGtvovn2TeCRVDI8Y9k61nY5w5rR5Mcdf1K9BA1wzP2L4nTBoHbur70eMdEmeM3R2e9LzFETmuUAFh7L1k6LDhx7kFqjnSLwPSVa8ALK1bJDjgv1i300NCo5divaY/mjIr9e2/AZWL3MQjdwceoVZPrpCgKfpp44XdMYB/fi/wDLORQkLIm5fQMznDeYZKGceILRTwWyjL8Yyy+bBfA++frNLF8Agknfm0gGEI9VBaF7TVYbDJrZ2lmdT68D1hagJ8g1vief7HArTgapHfLxLL2BYWmapEm284GowHDrg4hGHd1aZu+wIh10SzPp4tTGRp0scu/x4ZEr7cglKgegwy9L7ubFA7zm9E368Y6RMxYXETBGgeEVDAqVnfBHIOZVvBIEgsCw=" - skip_cleanup: true + secure: "gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII=" + skip_cleanup: true on: all_branches: true + deploy: + provider: releases + api_key: + secure: "Z/ewvydCLXEhlBBtQGYm2nZ8o+2RP+MwA5uEDuu6mEpZttUZAYaoHivChxADLXz8LNKvUloIeBeIL/PrLk6QnhSur/s2iEYHssrnl99SkAPtoWggyfsdacuKLMkpLoZGOBIEYKPuXuEZyqvugSUO42rSya1zdjcnXc4l+E/bXMc=" + file: _build/*.dmg + skip_cleanup: true + on: + tags: true + repo: coq/coq before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi diff --git a/API/API.ml b/API/API.ml index 1d7a4a4f46..c4bcef6f6c 100644 --- a/API/API.ml +++ b/API/API.ml @@ -169,7 +169,6 @@ module Stdarg = Stdarg module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops module Notation_ops = Notation_ops -module Ppextend = Ppextend module Notation = Notation module Dumpglob = Dumpglob (* module Syntax_def *) diff --git a/API/API.mli b/API/API.mli index 5804a82f64..d1774afe54 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3184,6 +3184,10 @@ sig | NCast of notation_constr * notation_constr Misctypes.cast_type type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * notation_constr + type precedence = int + type parenRelation = + | L | E | Any | Prec of precedence + type tolerability = precedence * parenRelation end module Tactypes : @@ -4013,18 +4017,11 @@ sig expand_evars : bool } - type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr - val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> - typing_constraint -> Glob_term.glob_constr -> pure_open_constr + typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr - val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit @@ -4179,16 +4176,6 @@ sig 'a -> Notation_term.notation_constr -> Glob_term.glob_constr end -module Ppextend : -sig - - type precedence = int - type parenRelation = - | L | E | Any | Prec of precedence - type tolerability = precedence * parenRelation - -end - module Notation : sig type cases_pattern_status = bool @@ -4393,16 +4380,16 @@ end module Evar_refiner : sig + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr + val w_refine : Evar.t * Evd.evar_info -> - Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map + glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map end module Proof_type : sig - type prim_rule = - | Cut of bool * bool * Names.Id.t * Term.types - | Refine of Constr.t + type prim_rule = Refine of Constr.t type tactic = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma end @@ -4880,7 +4867,7 @@ sig val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_lident : Names.Id.t Loc.located -> Pp.t val pr_lname : Names.Name.t Loc.located -> Pp.t - val prec_less : int -> int * Ppextend.parenRelation -> bool + val prec_less : int -> int * Notation_term.parenRelation -> bool val pr_constr_expr : Constrexpr.constr_expr -> Pp.t val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t @@ -5241,7 +5228,7 @@ sig val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> - EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.constr -> EConstr.constr val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> @@ -54,6 +54,7 @@ FIND_SKIP_DIRS:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' -o \ + -name 'user-contrib' -o \ -name 'coq-makefile' -o \ -name '.opamcache' -o \ -name '.coq-native' \ diff --git a/Makefile.build b/Makefile.build index 3d4b475dcd..92eaf7232d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -46,9 +46,6 @@ NO_RECALC_DEPS ?= # Non-empty runs the checker on all produced .vo files: VALIDATE ?= -# Is "-xml" when building XML library: -COQ_XML ?= - # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -189,7 +186,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) +COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) @@ -273,9 +270,6 @@ $(error This Makefile needs GNU Make 3.81 or later (that is a version that suppo endif VO_TOOLS_DEP := $(COQTOPBEST) -ifdef COQ_XML - VO_TOOLS_DEP += $(COQDOC) -endif ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) endif @@ -707,9 +701,9 @@ TIMING_EXTRA = endif theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) - $(SHOW)'COQC $(COQ_XML) -noinit $<' + $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) # MExtraction.v generates the ml core file of the micromega tactic. # We check that this generated code is still in sync with the version diff --git a/Makefile.common b/Makefile.common index afd6164fca..ccbe9261ef 100644 --- a/Makefile.common +++ b/Makefile.common @@ -105,7 +105,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma API/API.cma + parsing/highparsing.cma stm/stm.cma toplevel/toplevel.cma API/API.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/dev/README b/dev/README index 814f609576..b446c3e974 100644 --- a/dev/README +++ b/dev/README @@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- -Makefile.dir: makefile dedicated to intensive work in a given directory -Makefile.subdir: makefile dedicated to intensive work in a given subdirectory -Makefile.devel: utilities to automatically launch coq in various states -Makefile.common: used by other Makefiles objects.el: various development utilities at emacs level anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from diff --git a/dev/TODO b/dev/TODO deleted file mode 100644 index e62ee6e537..0000000000 --- a/dev/TODO +++ /dev/null @@ -1,22 +0,0 @@ - - o options de la ligne de commande - - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml - - o arguments implicites - - les calculer une fois pour toutes à la déclaration (dans Declare) - et stocker cette information dans le in_variable, in_constant, etc. - - o Environnements compilés (type Environ.compiled_env) - - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) - - o Efficacité - - utiliser DOPL plutôt que DOPN (sauf pour Case) - - batch mode => pas de undo, ni de reset - - conversion : déplier la constante la plus récente - - un cache pour type_of_const, type_of_inductive, type_of_constructor, - lookup_mind_specif - - o Toplevel - - parsing de la ligne de commande : utiliser Arg ??? - - diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index e8018158bf..b610f70004 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite ) diff --git a/dev/db_printers.ml b/dev/db_printers.ml deleted file mode 100644 index f4b4a425e2..0000000000 --- a/dev/db_printers.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -open Pp -open Names - -let pp s = pp (hov 0 s) - -let prid id = Format.print_string (Id.to_string id) -let prsp sp = Format.print_string (DirPath.to_string sp) - - diff --git a/dev/doc/api.txt b/dev/doc/api.txt deleted file mode 100644 index 5827257b53..0000000000 --- a/dev/doc/api.txt +++ /dev/null @@ -1,10 +0,0 @@ -Recommendations in using the API: - -The type of terms: constr (see kernel/constr.ml and kernel/term.ml) - -- On type constr, the canonical equality on CIC (up to - alpha-conversion and cast removal) is Constr.equal -- The type constr is abstract, use mkRel, mkSort, etc. to build - elements in constr; use "kind_of_term" to analyze the head of a - constr; use destRel, destSort, etc. when the head constructor is - known diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v index a81f170c63..a81f170c63 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion.v diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel deleted file mode 100644 index ffdb1bdca9..0000000000 --- a/dev/tools/Makefile.devel +++ /dev/null @@ -1,74 +0,0 @@ -# to be linked to makefile (lowercase - takes precedence over Makefile) -# in main directory -# make devel in main directory should do this for you. - -TOPDIR=. -BASEDIR= - -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API - -default: usage noargument - -usage:: - @echo Usage: make \<target\> - @echo Targets are: - -usage:: - @echo " setup-devel -- set the devel makefile" -setup-devel: - @ln -sfv dev/tools/Makefile.devel makefile - @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ - done) - - -usage:: - @echo " clean-devel -- clear all devel files" -clean-devel: - echo rm -f makefile .depend.devel - echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile) - - -usage:: - @echo " coqtop -- make until the bytecode executable, make the link" -coqtop: bin/coqtop.byte - ln -sf bin/coqtop.byte coqtop - - -usage:: - @echo " quick -- make bytecode executable and states" -quick: - $(MAKE) states BEST=byte - -include Makefile - -include $(TOPDIR)/dev/tools/Makefile.common - -# this file is better described in dev/tools/Makefile.dir -include .depend.devel - -#if dev/tools/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) -include $(TOPDIR)/dev/tools/Makefile.local -endif - - -usage:: - @echo " total -- runs coqtop with all theories required" -total: - ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th)))) - - -usage:: - @echo " run -- makes and runs bytecode coqtop using ledit and the history file" - @echo " if you want to pass arguments to coqtop, use make run ARG=<args>" -run: $(TOPDIR)/coqtop - ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS) - - -usage:: - @echo " vars -- echos commands to set COQTOP and COQBIN variables" -vars: - @(cd $(TOPDIR); \ - echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ ) diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir deleted file mode 100644 index 1a1bb90b44..0000000000 --- a/dev/tools/Makefile.dir +++ /dev/null @@ -1,131 +0,0 @@ -# make a link to this file if you are working hard in one directory of Coq -# ln -s ../dev/tools/Makefile.dir Makefile -# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead -# this Makefile provides many useful facilities to develop Coq -# it is not completely compatible with .ml4 files unfortunately - -ifndef TOPDIR -TOPDIR=.. -endif - -# this complicated thing should work for subsubdirs as well -BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||")) - -noargs: dir - -test-dir: - @echo TOPDIR=$(TOPDIR) - @echo BASEDIR=$(BASEDIR) - -include $(TOPDIR)/dev/tools/Makefile.common - -# make this directory -dir: - $(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR)) - -# make all cmo's in this directory. Useful in case the main Makefile is not -# up-to-date -all: - @( ( for i in *.ml; do \ - echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ - done; \ - for i in *.ml4; do \ - echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \ - done ) \ - | xargs $(MAKE) -C $(TOPDIR) ) - -# lists all files that should be compiled in this directory -list: - @(for i in *.mli; do \ - ls -l `basename $$i .mli`.cmi; \ - done) - @(for i in *.ml; do \ - ls -l `basename $$i .ml`.cmo; \ - done) - @(for i in *.ml4; do \ - ls -l `basename $$i .ml4`.cmo; \ - done) - - -clean:: - rm -f *.cmi *.cmo *.cmx *.o - - -# if grammar.cmo files cannot be compiled and main .depend cannot be -# rebuilt, this is quite useful -depend: - (cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel) - - -# displays the dependency graph of the current directory (vertically, -# unlike in doc/) -graph: - (ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) & - - -# the pretty entry draws a dependency graph marking red those nodes -# which do not have their .cmo files - -.INTERMEDIATE: depend.dot depend.2.dot -.PHONY: depend.ps - -depend.dot: - ocamldep *.ml *.mli | ocamldot > $@ - -depend.2.dot: depend.dot - (i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@ - (for ml in *.ml; do \ - base=`basename $$ml .ml`; \ - fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \ - rest=`echo $$base | cut -c2-`; \ - name=`echo $$fst $$rest | tr -d " "`; \ - cmo=$$base.cmo; \ - if [ ! -e $$cmo ]; then \ - echo \"$$name\" [color=red]\; >> $@;\ - fi;\ - done;\ - echo } >> $@) - -depend.ps: depend.2.dot - dot -Tps $< > $@ - -clean:: - rm -f depend.ps - -pretty: depend.ps - (gv -spartan $<; rm $<) & -# gv -spartan $< & - - - -# generating file.ml.mli by tricking make to pass -i to ocamlc - -%.ml.mli: FORCE - @(cmo=`basename $@ .ml.mli`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \ - echo Generated interface file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -%.annot: FORCE - @(cmo=`basename $@ .annot`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \ - echo Generated annotation file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -FORCE: - -clean:: - rm -f *.ml.mli - -# this is not perfect but mostly WORKS! It just calls the main makefile - -%.cmi: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -%.cmo: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -coqtop: - $(MAKE) -C $(TOPDIR) bin/coqtop.byte diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir deleted file mode 100644 index cb914bd129..0000000000 --- a/dev/tools/Makefile.subdir +++ /dev/null @@ -1,7 +0,0 @@ -# if you work in a sub/sub-rectory of Coq -# you should make a link to that makefile -# ln -s ../../dev/tools/Makefile.subdir Makefile -# in order to have all the facilities of dev/tools/Makefile.dir - -TOPDIR=../.. -include $(TOPDIR)/dev/tools/Makefile.dir diff --git a/dev/v8-syntax/.gitignore b/dev/v8-syntax/.gitignore new file mode 100644 index 0000000000..89e3509b00 --- /dev/null +++ b/dev/v8-syntax/.gitignore @@ -0,0 +1,6 @@ +# byproducts of check-grammar +def +df +use +use-k +use-t diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index fa2864cec9..6b7960c92f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} diff --git a/doc/Makefile.rt b/doc/Makefile.rt deleted file mode 100644 index 6c32813462..0000000000 --- a/doc/Makefile.rt +++ /dev/null @@ -1,43 +0,0 @@ -# Makefile for building Coq Technical Reports - -# if coqc,coqtop,coq-tex are not in your PATH, you need the environment -# variable COQBIN to be correctly set -# (COQTOP is autodetected) -# (some files are preprocessed using Coq and some part of the documentation -# is automatically built from the theories sources) - -# To compile documentation, you need the following tools: -# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils) -# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz) -# Pdf: pdflatex -# Html: -# - hevea: http://para.inria.fr/~maranget/hevea/ -# - htmlSplit: http://coq.inria.fr/~delahaye -# Rapports INRIA: dviselect, rrkit (par Michel Mauny) - -include ./Makefile - -################### -# RT -################### -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex - dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3: - (cd rt; $(LATEX) RefMan-cover.tex) - set a=`tail -1 refman/Reference-Manual.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - fi) - -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex - dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3: - (cd rt; $(LATEX) Tutorial-cover.tex) - set a=`tail -1 tutorial/Tutorial.v.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - fi) diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v index 8cfeebc28b..4b0ab31254 100644 --- a/doc/RecTutorial/RecTutorial.v +++ b/doc/RecTutorial/RecTutorial.v @@ -1,3 +1,5 @@ +Unset Automatic Introduction. + Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3). @@ -69,13 +71,13 @@ Check (Prop::Set::nil). Require Import Bvector. -Print vector. +Print Vector.t. -Check (Vnil nat). +Check (Vector.nil nat). -Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)). +Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)). -Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))). +Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))). Lemma eq_3_3 : 2 + 1 = 3. Proof. @@ -146,6 +148,7 @@ Proof. intros; absurd (p < p); eauto with arith. Qed. +Require Extraction. Extraction max. @@ -300,8 +303,8 @@ Section Le_case_analysis. (HS : forall m, n <= m -> Q (S m)). Check ( match H in (_ <= q) return (Q q) with - | le_n => H0 - | le_S m Hm => HS m Hm + | le_n _ => H0 + | le_S _ m Hm => HS m Hm end ). @@ -317,16 +320,16 @@ Proof. Qed. Definition Vtail_total - (A : Type) (n : nat) (v : vector A n) : vector A (pred n):= -match v in (vector _ n0) return (vector A (pred n0)) with -| Vnil => Vnil A -| Vcons _ n0 v0 => v0 + (A : Type) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= +match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with +| Vector.nil _ => Vector.nil A +| Vector.cons _ _ n0 v0 => v0 end. -Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n). +Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). intros A n v; case v. simpl. - exact (Vnil A). + exact (Vector.nil A). simpl. auto. Defined. @@ -498,10 +501,8 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. +Fail exact typ. (* -Defined. - Error: Universe Inconsistency. *) Abort. @@ -920,7 +921,6 @@ Defined. Print minus_decrease. - Definition div_aux (x y:nat)(H: Acc lt x):nat. fix 3. intros. @@ -969,40 +969,40 @@ let rec div_aux x y = | Right -> div_aux (minus x y) y) *) -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros A v;inversion v. Abort. (* - Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> v = Vnil A. + Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> v = Vector.nil A. Toplevel input, characters 40281-40287 -> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A. +> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vector.nil A. > ^^^^^^ Error: In environment A : Set n : nat -v : vector A n +v : Vector.t A n e : n = 0 -The term "Vnil A" has type "vector A 0" while it is expected to have type - "vector A n" +The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type + "Vector.t A n" *) Require Import JMeq. (* On devrait changer Set en Type ? *) -Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> JMeq v (Vnil A). +Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> JMeq v (Vector.nil A). Proof. destruct v. auto. intro; discriminate. Qed. -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros a v;apply JMeq_eq. apply vector0_is_vnil_aux. @@ -1010,56 +1010,56 @@ Proof. Qed. -Implicit Arguments Vcons [A n]. -Implicit Arguments Vnil [A]. -Implicit Arguments Vhead [A n]. -Implicit Arguments Vtail [A n]. +Implicit Arguments Vector.cons [A n]. +Implicit Arguments Vector.nil [A]. +Implicit Arguments Vector.hd [A n]. +Implicit Arguments Vector.tl [A n]. -Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n. +Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. destruct n; intro v. - exact Vnil. - exact (Vcons (Vhead v) (Vtail v)). + exact Vector.nil. + exact (Vector.cons (Vector.hd v) (Vector.tl v)). Defined. -Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)). -Eval simpl in (fun (A:Type)(v:vector A 0) => v). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v). -Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v). +Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v). Proof. destruct v. reflexivity. reflexivity. Defined. -Theorem zero_nil : forall A (v:vector A 0), v = Vnil. +Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil. Proof. intros. - change (Vnil (A:=A)) with (Vid _ 0 v). + change (Vector.nil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined. Theorem decomp : - forall (A : Type) (n : nat) (v : vector A (S n)), - v = Vcons (Vhead v) (Vtail v). + forall (A : Type) (n : nat) (v : Vector.t A (S n)), + v = Vector.cons (Vector.hd v) (Vector.tl v). Proof. intros. - change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v). + change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v). apply Vid_eq. Defined. Definition vector_double_rect : - forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type), - P 0 Vnil Vnil -> - (forall n (v1 v2 : vector A n) a b, P n v1 v2 -> - P (S n) (Vcons a v1) (Vcons b v2)) -> - forall n (v1 v2 : vector A n), P n v1 v2. + forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type), + P 0 Vector.nil Vector.nil -> + (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 -> + P (S n) (Vector.cons a v1) (Vector.cons b v2)) -> + forall n (v1 v2 : Vector.t A n), P n v1 v2. induction n. intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2). auto. @@ -1069,24 +1069,23 @@ Defined. Require Import Bool. -Definition bitwise_or n v1 v2 : vector bool n := - vector_double_rect bool (fun n v1 v2 => vector bool n) - Vnil - (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2. - +Definition bitwise_or n v1 v2 : Vector.t bool n := + vector_double_rect bool (fun n v1 v2 => Vector.t bool n) + Vector.nil + (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2. -Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v} +Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with - _ , Vnil => None - | 0 , Vcons b _ _ => Some b - | S n', Vcons _ p' v' => vector_nth A n' p' v' + _ , Vector.nil => None + | 0 , Vector.cons b _ => Some b + | S n', @Vector.cons _ _ p' v' => vector_nth A n' p' v' end. Implicit Arguments vector_nth [A p]. -Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b, +Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, vector_nth i v1 = Some a -> vector_nth i v2 = Some b -> vector_nth i (bitwise_or _ v1 v2) = Some (orb a b). diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex deleted file mode 100644 index ac1686c25e..0000000000 --- a/doc/rt/RefMan-cover.tex +++ /dev/null @@ -1,45 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. - -\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1} -\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1 -\thanks -{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes, -Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez, -Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy, -Catherine Parent, Christine Paulin-Mohring, -Amokrane Sa{\"\i}bi, Benjamin Werner} -\authorhead{} -\titlehead{Coq V7.1 Reference Manual} -\RRtheme{2} -\RRprojet{Coq} -\RRNo{0123456789} -\RRdate{May 1997} -%\RRpages{} -\URRocq - -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue le manuel de r\'ef\'erence de la version V7.1 -qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, -Calcul des Constructions Inductives} - - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. -Coq V7.1 is available by anonymous -ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex deleted file mode 100644 index aefea8d429..0000000000 --- a/doc/rt/Tutorial-cover.tex +++ /dev/null @@ -1,47 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. -\RRetitle{ -The Coq Proof Assistant \\ A Tutorial \\ Version 7.1 -\thanks{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRtitle{Coq \\ Une introduction \\ V7.1 } -\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring} -\RRtheme{2} -\RRprojet{{Coq -\\[15pt] -{INRIA Rocquencourt} -{\hskip -5.25pt} -~~{\bf ---}~~ - \def\thefootnote{\arabic{footnote}\hss} -{CNRS - ENS Lyon} -\footnote[1]{LIP URA 1398 du CNRS, -46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.} -{\hskip -14pt}}} - -%\RRNo{0123456789} -\RRNo{0204} -\RRdate{Ao\^ut 1997} - -\URRocq -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue une introduction pratique \`a l'utilisation de -la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul -des Constructions Inductives} - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. This document is a -tutorial for the version V7.1 of Coq. This version is available by -anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index ed1d336d9e..3ee65d6f22 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints: \begin{itemize} \item compilation is achieved by invoking make without specifying a target \item options are passed to Coq with make variable COQFLAGS that - includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML. + includes variables OPT, COQLIBS, and OTHERFLAGS. \end{itemize} These constraints are met by the makefiles produced by {\tt coq\_makefile} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 2afc12cd36..339c6a248e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -412,6 +412,14 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) +let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in + let instance = + match filter with + | None -> instance + | Some filter -> Filter.filter_list filter instance in + new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance + (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = diff --git a/engine/evarutil.mli b/engine/evarutil.mli index a8b6b5861c..14173e774d 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -21,6 +21,13 @@ val new_meta : unit -> metavariable val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) + +val new_evar_from_context : + named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> evar_map * EConstr.t + val new_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 54861ae4cc..e85415bed3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args = let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) -let has_curly_brackets ntn = - String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 || - String.is_sub " { _ }" ntn (String.length ntn - 6) || - String.string_contains ~where:ntn ~what:" { _ } ") - -let rec wildcards ntn n = - if Int.equal n (String.length ntn) then [] - else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l -and spaces ntn n = - if Int.equal n (String.length ntn) then [] - else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1) - -let expand_curly_brackets loc mknot ntn l = - let ntn' = ref ntn in - let rec expand_ntn i = - function - | [] -> [] - | a::l -> - let a' = - let p = List.nth (wildcards !ntn' 0) i - 2 in - if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p - then begin - ntn' := - String.sub !ntn' 0 p ^ "_" ^ - String.sub !ntn' (p+5) (String.length !ntn' -p-5); - mknot (loc,"{ _ }",[a]) end - else a in - a' :: expand_ntn (i+1) l in - let l = expand_ntn 0 l in - (* side effect *) - mknot (loc,!ntn',l) - let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None @@ -367,9 +335,7 @@ let is_zero s = in aux 0 let make_notation_gen loc ntn mknot mkprim destprim l = - if has_curly_brackets ntn - then expand_curly_brackets loc mknot ntn l - else match ntn,List.map destprim l with + match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> mknot (loc,ntn,([mknot (loc,"( _ )",l)])) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c9fc3aa4f3..e465677cde 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2038,7 +2038,9 @@ let interp_constr_evars_gen_impls env evdref ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - understand_tcc_evars env evdref ~expected_type c, imps + let evd, c = understand_tcc env !evdref ~expected_type c in + evdref := evd; + c, imps let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c @@ -2053,7 +2055,9 @@ let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in - understand_tcc_evars env evdref ~expected_type c + let evd, c = understand_tcc env !evdref ~expected_type c in + evdref := evd; + c let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c @@ -2098,7 +2102,9 @@ let interp_binder env sigma na t = let interp_binder_evars env evdref na t = let t = intern_gen IsType env t in let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in - understand_tcc_evars env evdref ~expected_type:IsType t' + let evd, c = understand_tcc env !evdref ~expected_type:IsType t' in + evdref := evd; + c let my_intern_constr env lvar acc c = internalize env acc false lvar c @@ -2125,7 +2131,8 @@ let interp_glob_context_evars env evdref k bl = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t in - let t = understand_tcc_evars env evdref ~expected_type:IsType t' in + let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in + evdref := evd; match b with None -> let d = LocalAssum (na,t) in @@ -2137,7 +2144,8 @@ let interp_glob_context_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in + evdref := evd; let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) diff --git a/interp/declare.ml b/interp/declare.ml index 70f422b514..7fcb38296f 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -32,14 +32,6 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) -(** XML output hooks *) - -let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () -let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () -let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () - -let if_xml f x = if !Flags.xml_export then f x else () - (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -95,7 +87,6 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); - if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -256,7 +247,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] @@ -268,9 +258,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_kind = kind; cst_locl = local; } in - let kn = declare_constant_common id cst in - let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in - kn + declare_constant_common id cst let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) @@ -410,7 +398,6 @@ let declare_mind mie = let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; - if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) diff --git a/interp/declare.mli b/interp/declare.mli index 6a09434645..ccd7d28bb5 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -69,11 +69,6 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool -(** Hooks for XML output *) -val xml_declare_variable : (object_name -> unit) Hook.t -val xml_declare_constant : (internal_flag * constant -> unit) Hook.t -val xml_declare_inductive : (bool * object_name -> unit) Hook.t - (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/interp/notation.ml b/interp/notation.ml index c07a009438..c373faf680 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -41,7 +41,6 @@ open Context.Named.Declaration (**********************************************************************) (* Scope of symbols *) -type level = precedence * tolerability list type delimiters = string type notation_location = (DirPath.t * DirPath.t) * string @@ -83,11 +82,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with | Prec l1, Prec l2 -> Int.equal l1 l2 | _ -> false -let level_eq (l1, t1) (l2, t2) = +let notation_var_internalization_type_eq v1 v2 = match v1, v2 with +| NtnInternTypeConstr, NtnInternTypeConstr -> true +| NtnInternTypeBinder, NtnInternTypeBinder -> true +| NtnInternTypeIdent, NtnInternTypeIdent -> true +| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false + +let level_eq (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + && List.equal notation_var_internalization_type_eq u1 u2 let declare_scope scope = try let _ = String.Map.find scope !scope_map in () diff --git a/interp/notation.mli b/interp/notation.mli index e63ad10cde..f9f247fe10 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -21,7 +21,6 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list type delimiters = string type scope type scopes (** = [scope_name list] *) diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 2bbe87bbca..3ebc9b71d2 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -7,17 +7,10 @@ (************************************************************************) open Pp +open Notation_term (*s Pretty-print. *) -(* Dealing with precedences *) - -type precedence = int - -type parenRelation = L | E | Any | Prec of precedence - -type tolerability = precedence * parenRelation - type ppbox = | PpHB of int | PpHOVB of int diff --git a/interp/ppextend.mli b/interp/ppextend.mli index a347a5c7b7..6ff5a42728 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -6,15 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** {6 Pretty-print. } *) - -(** Dealing with precedences *) - -type precedence = int +open Notation_term -type parenRelation = L | E | Any | Prec of precedence - -type tolerability = precedence * parenRelation +(** {6 Pretty-print. } *) type ppbox = | PpHB of int diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cee96040bd..c342da3dca 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -88,11 +88,24 @@ type grammar_constr_prod_item = concat with last parsed list when true; additionally release the p last items as if they were parsed autonomously *) -type notation_grammar = { - notgram_level : int; +(** Dealing with precedences *) + +type precedence = int +type parenRelation = L | E | Any | Prec of precedence +type tolerability = precedence * parenRelation + +type level = precedence * tolerability list * notation_var_internalization_type list + +(** Grammar rules for a notation *) + +type one_notation_grammar = { + notgram_level : level; notgram_assoc : Extend.gram_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; +} + +type notation_grammar = { notgram_onlyprinting : bool; + notgram_rules : one_notation_grammar list } diff --git a/lib/flags.ml b/lib/flags.ml index 027ba16f0e..d4be81c61a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -87,8 +87,6 @@ let in_toplevel = ref false let profile = false -let xml_export = ref false - let ide_slave = ref false let ideslave_coqtop_flags = ref None @@ -96,7 +94,6 @@ let time = ref false let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 5af563b46e..3024c60396 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -56,11 +56,6 @@ val stm_debug : bool ref val profile : bool -(* Legacy flags *) - -(* -xml option: xml hooks will be called *) -val xml_export : bool ref - (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref diff --git a/library/declaremods.ml b/library/declaremods.ml index e7aa5bd0d6..6d9295bde8 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -557,17 +557,6 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" -(** XML output hooks *) - -let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () -let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () -let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () -let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () -let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () -let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () - -let if_xml f x = if !Flags.xml_export then f x else () - (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -589,7 +578,6 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - if_xml (Hook.get f_xml_start_module) mp; mp let end_module () = @@ -628,7 +616,6 @@ let end_module () = assert (eq_full_path (fst newoname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -682,7 +669,6 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); - if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -699,7 +685,6 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - if_xml (Hook.get f_xml_start_module_type) mp; mp let end_modtype () = @@ -716,7 +701,6 @@ let end_modtype () = assert (eq_full_path (fst oname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd oname)) mp); - if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -750,7 +734,6 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); - if_xml (Hook.get f_xml_declare_module_type) mp; mp end diff --git a/library/declaremods.mli b/library/declaremods.mli index 005594b8d8..9d750b6168 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -63,14 +63,6 @@ val start_modtype : val end_modtype : unit -> module_path -(** Hooks for XML output *) -val xml_declare_module : (module_path -> unit) Hook.t -val xml_start_module : (module_path -> unit) Hook.t -val xml_end_module : (module_path -> unit) Hook.t -val xml_declare_module_type : (module_path -> unit) Hook.t -val xml_start_module_type : (module_path -> unit) Hook.t -val xml_end_module_type : (module_path -> unit) Hook.t - (** {6 Libraries i.e. modules on disk } *) type library_name = DirPath.t diff --git a/library/lib.ml b/library/lib.ml index dc903df09d..5418003ebc 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -521,11 +521,6 @@ let is_in_section ref = (*************) (* Sections. *) - -(* XML output hooks *) -let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () -let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () - let open_section id = let olddir,(mp,oldsec) = !lib_state.path_prefix in let dir = add_dirpath_suffix olddir id in @@ -537,7 +532,6 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); lib_state := { !lib_state with path_prefix = prefix }; - if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -565,7 +559,6 @@ let close_section () = let full_olddir = fst !lib_state.path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); - if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index f1c9bfca24..3dcec1d53a 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -150,10 +150,6 @@ val unfreeze : frozen -> unit val init : unit -> unit -(** XML output hooks *) -val xml_open_section : (Names.Id.t -> unit) Hook.t -val xml_close_section : (Names.Id.t -> unit) Hook.t - (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list @@ -165,7 +161,7 @@ val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info val variable_section_segment_of_reference : Globnames.global_reference -> variable_context - + val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool diff --git a/library/library.ml b/library/library.ml index 20ecc2c229..28afa054e9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -551,8 +551,6 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) -let (f_xml_require, xml_require) = Hook.make ~default:ignore () - let warn_require_in_module = CWarnings.create ~name:"require-in-module" ~category:"deprecated" (fun () -> strbrk "Require inside a module is" ++ @@ -574,7 +572,6 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; () (* the function called by Vernacentries.vernac_import *) diff --git a/library/library.mli b/library/library.mli index 604167804d..6c624ce52f 100644 --- a/library/library.mli +++ b/library/library.mli @@ -67,9 +67,6 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Hook for the xml exportation of libraries } *) -val xml_require : (DirPath.t -> unit) Hook.t - (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound diff --git a/man/coqide.1 b/man/coqide.1 index f82bf2ad40..3592f6e4e3 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -123,13 +123,6 @@ Set sort Set impredicative. .TP .B \-dont\-load\-proofs Don't load opaque proofs in memory. -.TP -.B \-xml -Export XML files either to the hierarchy rooted in -the directory -.B COQ_XML_LIBRARY_ROOT -(if set) or to stdout (if unset). - .SH SEE ALSO diff --git a/man/coqtop.1 b/man/coqtop.1 index feee7fd8b5..62d17aa674 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -153,12 +153,6 @@ set sort Set impredicative .B \-dont\-load\-proofs don't load opaque proofs in memory -.TP -.B \-xml -export XML files either to the hierarchy rooted in -the directory $COQ_XML_LIBRARY_ROOT (if set) or to -stdout (if unset) - .SH SEE ALSO .BR coqc (1), diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 5fcbb43b6f..636027f9b4 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -368,9 +368,6 @@ let rec string loc ~comm_level bp len = parser let loc = set_loc_pos loc bp ep in err loc Unterminated_string -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - (* To associate locations to a file name *) let current_file = ref None @@ -432,9 +429,6 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current_comment in - if !Flags.xml_export && Buffer.length current_comment > 0 && - (!between_commands || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; (if !Flags.beautify && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 09c9d8ee45..77d652b185 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -19,9 +19,6 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit - -val xml_output_comment : (string -> unit) Hook.t - val terminal : string -> Tok.t (** The lexer of Coq: *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ec422c58db..870137ca11 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -443,7 +443,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = - let n = ng.notgram_level in + let n,_,_ = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key forpat n in let fold (accu, state) pt = @@ -464,7 +464,7 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () -let extend_constr_notation (_, ng) state = +let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> default_constr_levels | Some lev -> lev @@ -476,7 +476,7 @@ let extend_constr_notation (_, ng) state = let state = GramState.set state constr_levels levels in (r @ r', state) -let constr_grammar : (Notation.level * notation_grammar) grammar_command = +let constr_grammar : one_notation_grammar grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 248de3348e..8e0469275c 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -13,5 +13,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 93a778274d..560a9a7578 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,6 +51,19 @@ let make_bullet s = | '*' -> Star n | _ -> assert false +let parse_compat_version ?(allow_old = true) = let open Flags in function + | "8.8" -> Current + | "8.7" -> V8_7 + | "8.6" -> V8_6 + | "8.5" -> V8_5 + | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + if allow_old then VOld else + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + let extraction_err ~loc = if not (Mltop.module_is_known "extraction_plugin") then CErrors.user_err ~loc (str "Please do first a Require Extraction.") @@ -1168,7 +1181,7 @@ GEXTEND Gram [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> Some Flags.Current | "("; IDENT "compat"; s = STRING; ")" -> - Some (Coqinit.get_compat_version s) + Some (parse_compat_version s) | -> None ] ] ; obsolete_locality: @@ -1186,7 +1199,7 @@ GEXTEND Gram | IDENT "only"; IDENT "printing" -> SetOnlyPrinting | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetCompatVersion (Coqinit.get_compat_version s) + SetCompatVersion (parse_compat_version s) | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s]; s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] -> begin match s1, s2 with diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4934b0750b..11d3a6d1f4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -231,7 +231,8 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma = project gls in + let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in sigma, mkLambda(Name id,intype,body) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 6097951330..89feea8dcf 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -249,7 +249,7 @@ END let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t) ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index b06f35ddc4..00668ddc7d 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -64,7 +64,7 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) -> + (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f3f2f27e9e..b847aadf21 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Pretyping.type_uconstr ~flags ist c in + let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c = let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in - let c = Pretyping.type_uconstr ~flags ~expected_type ist c in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = begin fun sigma -> c env sigma end in diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 301943a509..5baa0d5c1d 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = expand_evars = true } in let map c env sigma = c env sigma in - List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 140cc33440..cb7d9b9c02 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -18,7 +18,7 @@ open Geninterp open Stdarg open Tacarg open Libnames -open Ppextend +open Notation_term open Misctypes open Locus open Decl_kinds diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 0bf9bc7f62..1f6ebaf448 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -16,7 +16,7 @@ open Misctypes open Environ open Constrexpr open Tacexpr -open Ppextend +open Notation_term type 'a grammar_tactic_prod_item_expr = | TacTerm of string diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d3e625e73a..51eed2f4ec 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None }) + ?(expected_type = WithoutTypeConstraint) ist c = + begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; + } in + understand_ltac flags env sigma vars expected_type term + end + let warn_deprecated_info = CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" (fun () -> diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 73e4f3d6ab..c1ab2b4c49 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -54,6 +54,11 @@ val set_debug : debug_info -> unit (** Gives the state of debug *) val get_debug : unit -> debug_info +val type_uconstr : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + (** Adds an interpretation function for extra generic arguments *) val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index ce23bb2b30..db1981228a 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -62,7 +62,7 @@ DECLARE PLUGIN "ssreflect_plugin" * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Ppextend.E) +let tacltop = (5,Notation_term.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 88beeaa711..f9dc345e15 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -10,11 +10,11 @@ val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c +val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd +val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b4d87dfdb0..40b8bcad92 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,8 +47,6 @@ open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) @@ -385,9 +383,6 @@ let adjust_evar_source evdref na c = end | _, _ -> c -(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -let allow_anonymous_refs = ref false - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j @@ -918,9 +913,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - List.map (set_name Anonymous) arsgn - else arsgn + List.map (set_name Anonymous) arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) @@ -981,10 +974,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn - else arsgn + (* Make dependencies from arity signature impossible *) + List.map (set_name Anonymous) arsgn in let nar = List.length arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in @@ -1018,13 +1009,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let csgn = - if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs_args - else - List.map (map_name (function Name _ as n -> n - | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs_args - in + List.map (set_name Anonymous) cs_args + in let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs_args in @@ -1191,29 +1177,6 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let on_judgment sigma f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast sigma (f c) in - {uj_val = c; uj_type = t} - -let understand_judgment env sigma c = - let env = make_env env sigma in - let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment sigma (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in - evdref := evd; c) j - in j, Evd.evar_universe_context !evdref - -let understand_judgment_tcc env evdref c = - let env = make_env env !evdref in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment !evdref (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in - evdref := evd; c) j - let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in @@ -1231,36 +1194,10 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in (sigma, c) -let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = - let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in - evdref := sigma; - c - let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = true; - use_hook = None; - fail_evar = true; - expand_evars = true } - -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - begin fun env sigma -> - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; - } in - understand_ltac flags env sigma vars expected_type term - end - let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6e533f1784..7395e94a09 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -27,9 +27,6 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * constr - type inference_hook = env -> evar_map -> evar -> evar_map * constr type inference_flags = { @@ -48,9 +45,6 @@ val all_no_fail_flags : inference_flags val all_and_fail_flags : inference_flags -(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -val allow_anonymous_refs : bool ref - (** Generic calls to the interpreter from glob_constr to open_constr; by default, inference_flags tell to use type classes and heuristics (but no external tactic solver hooks), as well as to @@ -61,9 +55,6 @@ val allow_anonymous_refs : bool ref val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr -val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> constr - (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -78,7 +69,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + typing_constraint -> glob_constr -> evar_map * EConstr.t (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; @@ -90,20 +81,6 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context -(** Idem but returns the judgment of the understood term *) - -val understand_judgment : env -> evar_map -> - glob_constr -> unsafe_judgment Evd.in_evar_universe_context - -(** Idem but do not fail on unresolved evars (type cl*) -val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> unsafe_judgment - -val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open - (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ee03bc9007..4a103cdd23 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -15,6 +15,7 @@ open Nameops open Libnames open Pputils open Ppextend +open Notation_term open Constrexpr open Constrexpr_ops open Decl_kinds @@ -737,7 +738,7 @@ let tag_var = tag Tag.variable pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Ppextend.precedence * Ppextend.parenRelation + type precedence = Notation_term.precedence * Notation_term.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 8335034851..7546c748d8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,6 +15,7 @@ open Libnames open Constrexpr open Names open Misctypes +open Notation_term val extract_lam_binders : constr_expr -> local_binder_expr list * constr_expr @@ -24,7 +25,7 @@ val split_fix : int -> constr_expr -> constr_expr -> local_binder_expr list * constr_expr * constr_expr -val prec_less : int -> int * Ppextend.parenRelation -> bool +val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index e9d104b491..28b10c7812 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -846,15 +846,6 @@ let pr_goal_by_uid uid = (* Elementary tactics *) let pr_prim_rule = function - | Cut (b,replace,id,t) -> - if b then - (* TODO: express "replace" *) - (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") - else - let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ - str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | Refine c -> (** FIXME *) str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index cc81adb853..48fa2202ee 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -13,11 +13,14 @@ open Evd open Evarutil open Evarsolve open Pp +open Glob_term (******************************************) (* Instantiation of existential variables *) (******************************************) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let t1 = EConstr.of_constr t1 in let t2 = EConstr.of_constr t2 in diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b65ffb1bee..5d69715967 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -7,9 +7,11 @@ (************************************************************************) open Evd -open Pretyping +open Glob_term (** Refinement of existential variables. *) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index 17128b92e1..20d075ae14 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -22,7 +22,6 @@ open Proof_type open Type_errors open Retyping open Misctypes -open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -93,15 +92,6 @@ let check_typability env sigma c = (* Implementation of the structural rules (moving and deleting hypotheses around) *) -(* The Clear tactic: it scans the context for hypotheses to be removed - (instead of iterating on the list of identifier to be removed, which - forces the user to give them in order). *) - -let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - (* The ClearBody tactic *) (* Reordering of the context *) @@ -200,14 +190,6 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let rec get_hyp_after h = function - | [] -> error_no_such_hypothesis h - | d :: right -> - if Id.equal (NamedDecl.get_id d) h then - match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst - else - get_hyp_after h right - let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom @@ -282,6 +264,10 @@ let move_hyp_in_named_context sigma hfrom hto sign = split_sign hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto +let insert_decl_in_named_context sigma decl hto sign = + let open EConstr in + move_hyp sigma false ([],decl,named_context_of_val sign) hto + (**********************************************************************) @@ -535,37 +521,9 @@ let convert_hyp check sign sigma d = (* Primitive tactics are handled here *) let prim_refiner r sigma goal = - let env = Goal.V82.env sigma goal in - let sign = Goal.V82.hyps sigma goal in let cl = Goal.V82.concl sigma goal in - let mk_goal hyps concl = - Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) - in - let open EConstr in match r with (* Logical rules *) - | Cut (b,replace,id,t) -> -(* if !check && not (Retyping.get_sort_of env sigma t) then*) - let t = EConstr.of_constr t in - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in - let sign,t,cl,sigma = - if replace then - let nexthyp = get_hyp_after id (named_context_of_val sign) in - let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) - nexthyp, - t,cl,sigma - else - (if !check && mem_named_context_val id sign then - user_err ~hdr:"Logic.prim_refiner" - (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in - let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in - let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in - if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | Refine c -> let cl = EConstr.Unsafe.to_constr cl in check_meta_variables c; diff --git a/proofs/logic.mli b/proofs/logic.mli index 84a21044b2..9d0756b332 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -52,6 +52,8 @@ type refiner_error = exception RefinerError of refiner_error +val error_no_such_hypothesis : Id.t -> 'a + val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> @@ -59,3 +61,7 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map -> val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val + +val insert_decl_in_named_context : Evd.evar_map -> + EConstr.named_declaration -> Id.t Misctypes.move_location -> + Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 11f1a13e6e..2ad5f607f2 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -9,14 +9,12 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Names open Term (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) type prim_rule = - | Cut of bool * bool * Id.t * types | Refine of constr (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2ed9416d10..a4d662e0ae 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -115,22 +115,12 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c let refiner = refiner -let internal_cut_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (true,replace,id,t)) gl - -let internal_cut_rev_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (false,replace,id,t)) gl - let refine_no_check c gl = let c = EConstr.Unsafe.to_constr c in refiner (Refine c) gl (* Versions with consistency checks *) -let internal_cut b d t = with_check (internal_cut_no_check b d t) -let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 40b6573a15..93bf428fdc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -84,13 +84,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> types -> tactic -val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 371debede4..b98b103158 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1342,7 +1342,7 @@ module Search = struct | Some i -> str ", with depth limit " ++ int i)); tac - let run_on_evars p evm tac = + let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> @@ -1357,7 +1357,7 @@ module Search = struct let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply (Global.env ()) tac pv + Proofview.apply env tac pv in if Proofview.finished pv' then let evm' = Proofview.return pv' in @@ -1374,22 +1374,22 @@ module Search = struct else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found - let evars_eauto depth only_classes unique dep st hints p evd = + let evars_eauto env evd depth only_classes unique dep st hints p = let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in - let res = run_on_evars p evd eauto_tac in + let res = run_on_evars env evd p eauto_tac in match res with | None -> evd | Some evd' -> evd' - let typeclasses_eauto ?depth unique st hints p evd = - evars_eauto depth true unique false st hints p evd + let typeclasses_eauto env evd ?depth unique st hints p = + evars_eauto env evd depth true unique false st hints p (** Typeclasses eauto is an eauto which tries to resolve only goals of typeclass type, and assumes that the initially selected evars in evd are independent of the rest of the evars *) - let typeclasses_resolve debug depth unique p evd = + let typeclasses_resolve env evd debug depth unique p = let db = searchtable_map typeclasses_db in - typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd + typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p end (** Binding to either V85 or Search implementations. *) @@ -1532,7 +1532,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = if get_typeclasses_legacy_resolution () then V85.resolve_all_evars_once debug depth unique p evd else - Search.typeclasses_resolve debug depth unique p evd + Search.typeclasses_resolve env evd debug depth unique p in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 65864bd472..2b5bbfcd1b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -86,16 +86,16 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl -let out_term = function +let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = let (sigma, c) = c (pf_env gl) (project gl) in let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term c + out_term (pf_env gl) c in let l = List.map map l in try (prolog l n gl) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d4cad3fa89..e16fcec7c7 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -155,9 +155,9 @@ open Proofview.Notations (* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) -let match_eqdec sigma c = +let match_eqdec env sigma c = try - let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in + let (eqonleft,_,c1,c2,ty) = match_eqdec env sigma c in let (op,eq1,noteq,eq2) = match EConstr.kind sigma c with | App (op,[|ty1;ty2|]) -> @@ -202,8 +202,9 @@ let solveEqBranch rectype = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in @@ -229,8 +230,9 @@ let decideGralEquality = begin Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in + let env = Proofview.Goal.env gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> + match_eqdec env sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> let headtyp = hd_app sigma (pf_compute gl typ) in begin match EConstr.kind sigma headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi diff --git a/tactics/equality.ml b/tactics/equality.ml index 66345ce43c..ad6abfa1f6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,25 +334,27 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo (* Do we have a JMeq instance on twice the same domains ? *) -let jmeq_same_dom gl = function +let jmeq_same_dom env sigma = function | None -> true (* already checked in Hipattern.find_eq_data_decompose *) | Some t -> - let rels, t = decompose_prod_assum (project gl) t in - let env = push_rel_context rels (Proofview.Goal.env gl) in - match decompose_app (project gl) t with - | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2 + let rels, t = decompose_prod_assum sigma t in + let env = push_rel_context rels env in + match decompose_app sigma t with + | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2 | _ -> false (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) -let find_elim hdcncl lft2rgt dep cls ot gl = +let find_elim hdcncl lft2rgt dep cls ot = + Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in let is_global gr c = Termops.is_global sigma gr c in let inccl = Option.is_empty cls in + let env = Proofview.Goal.env gl in if (is_global Coqlib.glob_eq hdcncl || (is_global Coqlib.glob_jmeq hdcncl && - jmeq_same_dom gl ot)) && not dep + jmeq_same_dom env sigma ot)) && not dep then let c = match EConstr.kind sigma hdcncl with @@ -382,9 +384,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - let elim = EConstr.of_constr elim in - (sigma, (elim, Safe_typing.empty_private_constants)) + pf_constr_of_global (ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -400,14 +400,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl = in match EConstr.kind sigma hdcncl with | Ind (ind,u) -> + let c, eff = find_scheme scheme_name ind in - (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let (sigma, elim) = - fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) - in - let elim = EConstr.of_constr elim in - (sigma, (elim, eff)) + Proofview.tclEFFECTS eff <*> + pf_constr_of_global (ConstRef c) | _ -> assert false + end let type_of_clause cls gl = match cls with | None -> Proofview.Goal.concl gl @@ -420,9 +418,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun evd c type_of_cls in - let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.tclEFFECTS effs <*> + find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} @@ -536,7 +532,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let do_hyps = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) let ids gl = - let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in + let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in let ids_of_hyps = pf_ids_of_hyps gl in Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps in @@ -858,7 +854,8 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") + in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in let (mib,mip) = lookup_mind_specif env ind in @@ -880,7 +877,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -925,23 +922,20 @@ let build_selector env sigma dirn c ind special default = let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - sigma, mkCase (ci, p, c, Array.of_list brl) + mkCase (ci, p, c, Array.of_list brl) -let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ()) -let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ()) -let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ()) +let build_coq_False () = pf_constr_of_global (build_coq_False ()) +let build_coq_True () = pf_constr_of_global (build_coq_True ()) +let build_coq_I () = pf_constr_of_global (build_coq_I ()) -let rec build_discriminator env sigma dirn c = function +let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - let sigma, true_0 = build_coq_True sigma in - let sigma, false_0 = build_coq_False sigma in build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> - let sigma, false_0 = build_coq_False sigma in let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let sigma, subval = build_discriminator cnum_env sigma dirn newc l in + let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in kont sigma subval (false_0,mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is @@ -984,14 +978,15 @@ let ind_scheme_of_eq lbeq = ConstRef c, eff -let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = - let sigma, i = build_coq_I sigma in - let sigma, absurd_term = build_coq_False sigma in +let discrimination_pf e (t,t1,t2) discriminator lbeq = + build_coq_I () >>= fun i -> + build_coq_False () >>= fun absurd_term -> let eq_elim, eff = ind_scheme_of_eq lbeq in - let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in - let eq_elim = EConstr.of_constr eq_elim in - sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), - eff + Proofview.tclEFFECTS eff <*> + pf_constr_of_global eq_elim >>= fun eq_elim -> + Proofview.tclUNIT + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) + let eq_baseid = Id.of_string "e" @@ -1005,19 +1000,24 @@ let apply_on_clause (f,t) clause = clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = + build_coq_True () >>= fun true_0 -> + build_coq_False () >>= fun false_0 -> let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - let sigma, discriminator = - build_discriminator e_env sigma dirn (mkVar e) cpath in - let sigma,(pf, absurd_term), eff = - discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in - let pf_ty = mkArrow eqn absurd_term in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - Proofview.Unsafe.tclEVARS sigma <*> - Proofview.tclEFFECTS eff <*> - tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + let discriminator = + try + Proofview.tclUNIT + (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + with + UserError _ as ex -> Proofview.tclZERO ex + in + discriminator >>= fun discriminator -> + discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> + let pf_ty = mkArrow eqn absurd_term in + let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in + let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + tclTHENS (assert_after Anonymous absurd_term) + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1303,7 +1303,7 @@ let rec build_injrec env sigma dflt c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in - let sigma, res = kont sigma subval (dfltval,tuplety) in + let res = kont sigma subval (dfltval,tuplety) in sigma, (res, tuplety,dfltval) with UserError _ -> failwith "caught" @@ -1536,7 +1536,7 @@ let decomp_tuple_term env sigma c t = let rec decomprec inner_code ex exty = let iterated_decomp = try - let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in + let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose env sigma ex in let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code]) and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in let cdrtyp = beta_applist sigma (p,[car]) in diff --git a/tactics/equality.mli b/tactics/equality.mli index 421f7c7f5d..a4d1c0f9bd 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> evar_map * constr + constr -> constr -> constr diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 4101004d48..b057cf72bc 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -280,10 +280,7 @@ let coq_refl_jm_pattern = open Globnames -let is_matching sigma x y = is_matching (Global.env ()) sigma x y -let matches sigma x y = matches (Global.env ()) sigma x y - -let match_with_equation sigma t = +let match_with_equation env sigma t = if not (isApp sigma t) then raise NoEquationFound; let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with @@ -302,11 +299,11 @@ let match_with_equation sigma t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then + if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -335,8 +332,8 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) (** X1 -> X2 **) let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2")) -let match_arrow_pattern sigma t = - let result = matches sigma coq_arrow_pattern t in +let match_arrow_pattern env sigma t = + let result = matches env sigma coq_arrow_pattern t in match Id.Map.bindings result with | [(m1,arg);(m2,mind)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) @@ -349,13 +346,13 @@ let match_with_imp_term sigma c = let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) -let match_with_nottype sigma t = +let match_with_nottype env sigma t = try - let (arg,mind) = match_arrow_pattern sigma t in + let (arg,mind) = match_arrow_pattern env sigma t in if is_empty_type sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None -let is_nottype sigma t = op2bool (match_with_nottype sigma t) +let is_nottype env sigma t = op2bool (match_with_nottype env sigma t) (* Forall *) @@ -481,7 +478,7 @@ let dest_nf_eq gls eqn = (*** Sigma-types *) -let match_sigma sigma ex = +let match_sigma env sigma ex = match EConstr.kind sigma ex with | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) @@ -489,19 +486,19 @@ let match_sigma sigma ex = build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure -let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) - match_sigma ex +let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *) + match_sigma env ex (* Pattern "(sig ?1 ?2)" *) let coq_sig_pattern = lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"])) -let match_sigma sigma t = - match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with +let match_sigma env sigma t = + match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with | [(_,a); (_,p)] -> (a,p) | _ -> anomaly (Pp.str "Unexpected pattern.") -let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t +let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pattern) t (*** Decidable equalities *) @@ -533,15 +530,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true let op_or = coq_or_ref let op_sum = coq_sumbool_ref -let match_eqdec sigma t = +let match_eqdec env sigma t = let eqonleft,op,subst = - try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t + try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t with PatternMatchingFailure -> - try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t + try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t with PatternMatchingFailure -> - try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t + try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t with PatternMatchingFailure -> - false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in + false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Lazy.force op, c1, c2, typ @@ -551,8 +548,8 @@ let match_eqdec sigma t = let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole])) let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref))) -let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t -let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t +let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t +let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t (* Remark: patterns that have references to the standard library must be evaluated lazily (i.e. at the time they are used, not a the time diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 59406e1584..8ff6fe95c6 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -81,8 +81,8 @@ val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function val is_equality_type : testing_function -val match_with_nottype : (constr * constr) matching_function -val is_nottype : testing_function +val match_with_nottype : Environ.env -> (constr * constr) matching_function +val is_nottype : Environ.env -> testing_function val match_with_forall_term : (Name.t * constr * constr) matching_function val is_forall_term : testing_function @@ -114,7 +114,7 @@ type equation_kind = exception NoEquationFound val match_with_equation: - evar_map -> constr -> coq_eq_data option * constr * equation_kind + Environ.env -> evar_map -> constr -> coq_eq_data option * constr * equation_kind (***** Destructing patterns bound to some theory *) @@ -132,21 +132,21 @@ val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_ki (** Match a term of the form [(existT A P t p)] Returns associated lemmas and [A,P,t,p] *) -val find_sigma_data_decompose : evar_map -> constr -> +val find_sigma_data_decompose : Environ.env -> evar_map -> constr -> coq_sigma_data * (EInstance.t * constr * constr * constr * constr) (** Match a term of the form [{x:A|P}], returns [A] and [P] *) -val match_sigma : evar_map -> constr -> constr * constr +val match_sigma : Environ.env -> evar_map -> constr -> constr * constr -val is_matching_sigma : evar_map -> constr -> bool +val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) -val is_matching_not : evar_map -> constr -> bool -val is_matching_imp_False : evar_map -> constr -> bool +val is_matching_not : Environ.env -> evar_map -> constr -> bool +val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 82d58074bc..67bc55d3fe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -436,19 +436,85 @@ let find_name mayrepl decl naming gl = match naming with id (**************************************************************) +(* Computing position of hypotheses for replacing *) +(**************************************************************) + +let get_next_hyp_position id = + let rec aux = function + | [] -> error_no_such_hypothesis id + | decl :: right -> + if Id.equal (NamedDecl.get_id decl) id then + match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst + else + aux right + in + aux + +let get_previous_hyp_position id = + let rec aux dest = function + | [] -> error_no_such_hypothesis id + | decl :: right -> + let hyp = NamedDecl.get_id decl in + if Id.equal hyp id then dest else aux (MoveAfter hyp) right + in + aux MoveLast + +(**************************************************************) (* Cut rule *) (**************************************************************) +let clear_hyps2 env sigma ids sign t cl = + try + let evdref = ref (Evd.clear_metas sigma) in + let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in + (hyps, t, cl, !evdref) + with Evarutil.ClearDependencyError (id,err) -> + error_replacing_dependency env sigma id err + +let internal_cut_gen ?(check=true) dir replace id t = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let store = Proofview.Goal.extra gl in + let sign = named_context_val env in + let sign',t,concl,sigma = + if replace then + let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in + sign',t,concl,sigma + else + (if check && mem_named_context_val id sign then + user_err (str "Variable " ++ pr_id id ++ str " is already declared."); + push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in + let nf_t = nf_betaiota sigma t in + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let (sigma,ev,ev') = + if dir then + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + (sigma,ev,ev') + else + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + (sigma,ev,ev') in + let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in + (sigma, term) + end) + end + +let internal_cut ?(check=true) = internal_cut_gen ~check true +let internal_cut_rev ?(check=true) = internal_cut_gen ~check false + let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENLAST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut b id t) (tac id) end @@ -463,11 +529,7 @@ let assert_after_then_gen b naming t tac = Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENFIRST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut_rev b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut_rev b id t) (tac id) end @@ -999,29 +1061,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = in aux n [] -let get_next_hyp_position id gl = - let rec aux = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - if Id.equal (NamedDecl.get_id decl) id then - match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast - else - aux right - in - aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - -let get_previous_hyp_position id gl = - let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - let hyp = NamedDecl.get_id decl in - if Id.equal hyp id then dest else aux (MoveAfter hyp) right - in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - let intro_replacing id = Proofview.Goal.enter begin fun gl -> - let next_hyp = get_next_hyp_position id gl in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let next_hyp = get_next_hyp_position id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1040,7 +1083,8 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1053,7 +1097,8 @@ let intros_possibly_replacing ids = (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -2578,7 +2623,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else get_previous_hyp_position id gl in + else + get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -3074,17 +3120,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) -let warn_unused_intro_pattern = +let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" (fun names -> strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names) + (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) -let check_unused_names names = +let check_unused_names env sigma names = if not (List.is_empty names) then - warn_unused_intro_pattern names + warn_unused_intro_pattern env sigma names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous @@ -3204,8 +3250,12 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = peel_tac ra' dests names thin) end | [] -> - check_unused_names names; + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + check_unused_names env sigma names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) + end in peel_tac ra dests names [] @@ -3272,7 +3322,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3805,11 +3855,12 @@ let compare_upto_variables sigma x y = in compare x y -let specialize_eqs id gl = +let specialize_eqs id = let open Context.Rel.Declaration in - let env = Tacmach.pf_env gl in - let ty = Tacmach.pf_get_hyp_typ gl id in - let evars = ref (project gl) in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let ty = Tacmach.New.pf_get_hyp_typ id gl in + let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 in @@ -3852,16 +3903,18 @@ let specialize_eqs id gl = and acc' = Tacred.whd_simpl env !evars acc' in let ty' = Evarutil.nf_evar !evars ty' in if worked then - tclTHENFIRST (Tacmach.internal_cut true id ty') - (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl - else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl - + Tacticals.New.tclTHENFIRST + (internal_cut true id ty') + (exact_no_check ((* refresh_universes_strict *) acc')) + else + Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) + end let specialize_eqs id = Proofview.Goal.enter begin fun gl -> let msg = str "Specialization not allowed on dependent hypotheses" in Proofview.tclOR (clear [id]) (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> - Proofview.V82.tactic (specialize_eqs id) + specialize_eqs id end let occur_rel sigma n c = @@ -4485,7 +4538,7 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) - let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in + let x = id_of_name_using_hdchar env evd t Anonymous in new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then @@ -4521,8 +4574,9 @@ let induction_gen_l isrec with_evars elim names lc = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in + Proofview.tclENV >>= fun env -> let x = - id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in let id = new_fresh_id [] x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in @@ -4741,8 +4795,9 @@ let prove_symmetry hdcncl eq_kind = one_constructor 1 NoBindings ]) let match_with_equation sigma c = + Proofview.tclENV >>= fun env -> try - let res = match_with_equation sigma c in + let res = match_with_equation env sigma c in Proofview.tclUNIT res with NoEquationFound -> Proofview.tclZERO NoEquationFound diff --git a/test-suite/Makefile b/test-suite/Makefile index 1268ed14bc..78d90aad81 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -528,8 +528,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR f=`basename $*`; \ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ - diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ - grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \ + diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ + grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ if [ $$R = 0 -a $$S = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v deleted file mode 100644 index fce671c754..0000000000 --- a/test-suite/bugs/closed/5469.v +++ /dev/null @@ -1,3 +0,0 @@ -(* Some problems with the special treatment of curly braces *) - -Reserved Notation "'a' { x }" (at level 0, format "'a' { x }"). diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v new file mode 100644 index 0000000000..f02eae69c2 --- /dev/null +++ b/test-suite/bugs/closed/5608.v @@ -0,0 +1,33 @@ +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). +Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). + +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Inductive base_type := TZ | TWord (logsz : nat). +Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type). +Context {var : base_type -> Type}. +Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : +flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type +interp_base_type y) + end. +Inductive exprf : flat_type -> Type := +| Var {t} (v : var t) : exprf (Tbase t) +| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : +exprf tC +| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). +Global Arguments Var {_} _. +Global Arguments LetIn {_} _ {_} _. +Global Arguments Pair {_} _ {_} _. +Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A +(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Definition foo := + (fun x3 => + (LetIn (Var x3) (fun x18 : var TZ + => (Pair (Var x18) (Var x18))))). +Print foo. diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 39a7103d1b..40abb215e9 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9ae74fd67..e5dbfcb4be 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -1,3 +1,5 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set [<0, 2 >] : nat * nat * (nat * nat) [<0, 2 >] @@ -109,9 +111,14 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) -{0, 1} +{{0, 1}} : nat * nat -{0, 1, 2} +{{0, 1, 2}} : nat * (nat * nat) -{0, 1, 2, 3} +{{0, 1, 2, 3}} : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dee0f70f79..b1015137d6 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -1,4 +1,9 @@ (**********************************************************************) +(* Check precedence, spacing, etc. in printing with curly brackets *) + +Check {x|x=0}+{True/\False}+{forall x, x=0}. + +(**********************************************************************) (* Check printing of notations with several instances of a recursive pattern *) (* Was wrong but I could not trigger a problem due to the collision between *) (* different instances of ".." *) @@ -161,10 +166,23 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). -(**********************************************************************) (* Test recursive notations with the recursive pattern repeated on the right *) -Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). -Check {0,1}. -Check {0,1,2}. -Check {0,1,2,3}. +Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..). +Check {{0,1}}. +Check {{0,1,2}}. +Check {{0,1,2,3}}. + +(* Test printing of #5608 *) + +Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := + (let x:=a in ( .. (b0,b1) .., b2)). +Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 0ed5b524f3..4e36dec15b 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -16,3 +16,14 @@ eremember (S (S ?[x])). instantiate (x:=0). reflexivity. Qed. + +(* Don't know if it is good or not but the compatibility tells that + the asserted goal to prove is subject to beta-iota but not the + asserted hypothesis *) + +Goal True. +assert ((fun x => x) False). +Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) +2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) +Abort. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1d35f1ef6c..29e373eaa5 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -337,3 +337,14 @@ Goal True. evar (0=0). Abort. +(* Test location of hypothesis in "symmetry in H". This was broken in + 8.6 where H, when the oldest hyp, was moved at the place of most + recent hypothesis *) + +Goal 0=1 -> True -> True. +intros H H0. +symmetry in H. +(* H should be the first hypothesis *) +match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *) +exact (eq_refl H0). +Abort. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index e67ae6a925..5e8d2faa58 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -66,6 +66,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99). (** Notations for sigma-types or subsets *) +Reserved Notation "{ A } + { B }" (at level 50, left associativity). +Reserved Notation "A + { B }" (at level 50, left associativity). + Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). diff --git a/tools/beautify-archive b/tools/beautify-archive index 6bfa974a53..a327ea44e1 100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE cd $NEWARCHIVE rm description || true make clean -make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ +make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \ { echo ---- Failed to beautify; exit 1; } echo -------- Upgrading files in the beautification directory -------------- beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` diff --git a/tools/check-translate b/tools/check-translate index 3dd8240532..acb6f45903 100755 --- a/tools/check-translate +++ b/tools/check-translate @@ -2,7 +2,7 @@ echo -------------- Producing translated files --------------------- rm */*/*.v8 >& /dev/null -make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; } if [ -e translated ]; then rm -r translated; fi if [ -e successful-translation ]; then rm -r successful-translation; fi if [ -e failed-translation ]; then rm -r failed-translation; fi diff --git a/tools/coqc.ml b/tools/coqc.ml index 4595af6e88..862225d3d1 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -94,7 +94,7 @@ let parse_args () = | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet" - |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit" + |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 8ba6156709..1bbf76490d 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -117,7 +117,7 @@ let find_module m = if Hashtbl.mem local_modules m then Local else - try External (Filename.concat (find_external_library m) m) + try External (find_external_library m ^ "/" ^ m) with Not_found -> Unknown diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 326ef54715..5ca8869655 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -125,15 +125,3 @@ let init_ocaml_path () = in Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir Coq_config.all_src_dirs - -let get_compat_version ?(allow_old = true) = function - | "8.8" -> Flags.Current - | "8.7" -> Flags.V8_7 - | "8.6" -> Flags.V8_6 - | "8.5" -> Flags.V8_5 - | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - if allow_old then Flags.VOld else - CErrors.user_err ~hdr:"get_compat_version" - (str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> CErrors.user_err ~hdr:"get_compat_version" - (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index bf8558d10a..3432e79cc0 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -24,5 +24,3 @@ val init_load_path : unit -> unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit - -val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8fe27b3b97..0f8524e923 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -516,7 +516,7 @@ let parse_args arglist = Flags.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> - let v = get_compat_version ~allow_old:false (next ()) in + let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) @@ -585,7 +585,6 @@ let parse_args arglist = |"-v"|"--version" -> Usage.version (exitcode ()) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true - |"-xml" -> Flags.xml_export := true (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 962bb4302b..d596e36f34 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -78,9 +78,6 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\n -xml export XML files either to the hierarchy rooted in\ -\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ -\n stdout (if unset)\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fe853c093d..bfab447706 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -243,10 +243,6 @@ let process_expr sid loc_ast = checknav_deep loc_ast; interp_vernac sid loc_ast -(* XML output hooks *) -let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () -let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () - let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> @@ -308,7 +304,6 @@ let compile verbosely f = ~v_file:long_f_dot_v); Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); - if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); @@ -318,7 +313,6 @@ let compile verbosely f = Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); - if !Flags.xml_export then Hook.get f_xml_end_library (); Dumpglob.end_dump_glob () | BuildVio -> let long_f_dot_v = ensure_v f in diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 77c4f44e12..bccf560e16 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -21,7 +21,3 @@ val load_vernac : bool -> Stateid.t -> string -> Stateid.t (** Compile a vernac file, (f is assumed without .v suffix) *) val compile : bool -> string -> unit - -(** Set XML hooks *) -val xml_start_library : (unit -> unit) Hook.t -val xml_end_library : (unit -> unit) Hook.t diff --git a/vernac/command.ml b/vernac/command.ml index e04bebe33b..a315ac14e2 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -393,8 +393,9 @@ let is_impredicative env u = let interp_ind_arity env evdref ind = let c = intern_gen IsType env ind.ind_arity in - let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in + let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in + evdref := evd; let pseudo_poly = check_anonymous_type c in let () = if not (Reductionops.is_arity env !evdref t) then user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c0974d0a7c..8b042a3ca3 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -522,35 +522,11 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let warn_skip_spaces_curly = - CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" - (fun () ->strbrk "Skipping spaces inside curly brackets") - -let rec drop_spacing = function - | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt - | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt - | fmt -> fmt - -let has_closing_curly_brace symbs fmt = - (* TODO: recognize and fail in case a box overlaps a pair of curly braces *) - let fmt = drop_spacing fmt in - match symbs, fmt with - | NonTerminal s :: symbs, (UnpTerminal s' as u) :: fmt when Id.equal s (Id.of_string s') -> - let fmt = drop_spacing fmt in - (match fmt with - | UnpTerminal "}" :: fmt -> Some (u :: fmt) - | _ -> None) - | _ -> None - let hunks_of_format (from,(vars,typs)) symfmt = - let a = ref None in let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when String.equal s' (String.make (String.length s') ' ') -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | symbs, (UnpTerminal "{") :: fmt when (a := has_closing_curly_brace symbs fmt; !a <> None) -> - let newfmt = Option.get !a in - aux (symbs,newfmt) | Terminal s :: symbs, (UnpTerminal s') :: fmt when String.equal s (String.drop_simple_quotes s') -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l @@ -705,26 +681,40 @@ let recompute_assoc typs = (**************************************************************************) (* Registration of syntax extensions (parsing/printing, no interpretation)*) -let pr_arg_level from = function +let pr_arg_level from (lev,typ) = + let pplev = match lev with | (n,L) when Int.equal n from -> str "at next level" | (n,E) -> str "at level " ++ int n | (n,L) -> str "at level below " ++ int n | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" - -let pr_level ntn (from,args) = + | (n,_) -> str "Unknown level" in + let pptyp = match typ with + | NtnInternTypeConstr -> mt () + | NtnInternTypeBinder -> str " " ++ surround (str "binder") + | NtnInternTypeIdent -> str " " ++ surround (str "ident") in + pplev ++ pptyp + +let pr_level ntn (from,args,typs) = str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ - prlist_with_sep pr_comma (pr_arg_level from) args + prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs) let error_incompatible_level ntn oldprec prec = user_err - (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ + (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++ + pr_level ntn oldprec ++ + spc() ++ str "while it is now required to be" ++ spc() ++ + pr_level ntn prec ++ str ".") + +let error_parsing_incompatible_level ntn ntn' oldprec prec = + user_err + (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++ + str " which is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") type syntax_extension = { - synext_level : Notation.level; + synext_level : Notation_term.level; synext_notation : notation; synext_notgram : notation_grammar; synext_unparsing : unparsing list; @@ -736,7 +726,17 @@ let is_active_compat = function | None -> true | Some v -> 0 <= Flags.version_compare v !Flags.compat_version -type syntax_extension_obj = locality_flag * syntax_extension list +type syntax_extension_obj = locality_flag * syntax_extension + +let check_and_extend_constr_grammar ntn rule = + try + let ntn_for_grammar = rule.notgram_notation in + if String.equal ntn ntn_for_grammar then raise Not_found; + let prec = rule.notgram_level in + let oldprec = Notation.level_of_notation ntn_for_grammar in + if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + with Not_found -> + Egramcoq.extend_constr_grammar rule let cache_one_syntax_extension se = let ntn = se.synext_notation in @@ -744,31 +744,30 @@ let cache_one_syntax_extension se = let onlyprint = se.synext_notgram.notgram_onlyprinting in try let oldprec = Notation.level_of_notation ntn in - if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec + if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram end let cache_syntax_extension (_, (_, sy)) = - List.iter cache_one_syntax_extension sy + cache_one_syntax_extension sy let subst_parsing_rule subst x = x let subst_printing_rule subst x = x let subst_syntax_extension (subst, (local, sy)) = - let map sy = { sy with - synext_notgram = subst_parsing_rule subst sy.synext_notgram; + (local, { sy with + synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules }; synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - } in - (local, List.map map sy) + }) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -1049,13 +1048,10 @@ let remove_curly_brackets l = | Terminal "{" as t1 :: l -> let br,next = skip_break [] l in (match next with - | NonTerminal _ as x :: l' as l0 -> + | NonTerminal _ as x :: l' -> let br',next' = skip_break [] l' in (match next' with - | Terminal "}" as t2 :: l'' as l1 -> - if not (List.equal Notation.symbol_eq l l0) || - not (List.equal Notation.symbol_eq l' l1) then - warn_skip_spaces_curly (); + | Terminal "}" as t2 :: l'' -> if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' @@ -1067,6 +1063,8 @@ let remove_curly_brackets l = module SynData = struct + type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list + (* XXX: Document *) type syn_data = { @@ -1089,17 +1087,28 @@ module SynData = struct intern_typs : notation_var_internalization_type list; (* Notation data for parsing *) - - level : int; - syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) - symbol list; (* symbols *) + level : level; + pa_syntax_data : subentry_types * symbol list; + pp_syntax_data : subentry_types * symbol list; not_data : notation * (* notation *) - (int * parenRelation) list * (* precedence *) + level * (* level, precedence, types *) bool; (* needs_squash *) } end +let find_subentry_types n assoc etyps symbols = + let innerlevel = NumLevel 200 in + let typs = + find_symbols + (NumLevel n,BorderProd(Left,assoc)) + (innerlevel,InternalProd) + (NumLevel n,BorderProd(Right,assoc)) + symbols in + let sy_typs = List.map (set_entry_type etyps) typs in + let prec = List.map (assoc_of_type n) sy_typs in + sy_typs, prec + let compute_syntax_data df modifiers = let open SynData in let open NotationMods in @@ -1115,27 +1124,24 @@ let compute_syntax_data df modifiers = (* Notations for interp and grammar *) let ntn_for_interp = make_notation_key symbols in - let symbols' = remove_curly_brackets symbols in - let ntn_for_grammar = make_notation_key symbols' in - if not onlyprint then check_rule_productivity symbols'; - - (* Misc *) - let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in - let msgs,n = find_precedence mods.level mods.etyps symbols' in - let innerlevel = NumLevel 200 in - let typs = - find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) - symbols' in + let symbols_for_grammar = remove_curly_brackets symbols in + let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in + let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in + if not onlyprint then check_rule_productivity symbols_for_grammar; + let msgs,n = find_precedence mods.level mods.etyps symbols in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in - let sy_typs = List.map (set_entry_type etyps) typs in - let prec = List.map (assoc_of_type n) sy_typs in + let sy_typs, prec = + find_subentry_types n assoc etyps symbols in + let sy_typs_for_grammar, prec_for_grammar = + if need_squash then + find_subentry_types n assoc etyps symbols_for_grammar + else + sy_typs, prec in let i_typs = set_internalization_type sy_typs in - let sy_data = (sy_typs,symbols') in - let sy_fulldata = (ntn_for_grammar,prec,need_squash) in + let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in + let pp_sy_data = (sy_typs,symbols) in + let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in let i_data = ntn_for_interp, df' in @@ -1154,8 +1160,9 @@ let compute_syntax_data df modifiers = mainvars; intern_typs = i_typs; - level = n; - syntax_data = sy_data; + level = (n,prec,i_typs); + pa_syntax_data = pa_sy_data; + pp_syntax_data = pp_sy_data; not_data = sy_fulldata; } @@ -1236,25 +1243,9 @@ let with_syntax_protection f x = (**********************************************************************) (* Recovering existing syntax *) -let contract_notation ntn = - if String.equal ntn "{ _ }" then ntn else - let rec aux ntn i = - if i <= String.length ntn - 5 then - let ntn' = - if String.is_sub "{ _ }" ntn i && - (i = 0 || ntn.[i-1] = ' ') && - (i = String.length ntn - 5 || ntn.[i+5] = ' ') - then - String.sub ntn 0 i ^ "_" ^ - String.sub ntn (i+5) (String.length ntn -i-5) - else ntn in - aux ntn' (i+1) - else ntn in - aux ntn 0 - exception NoSyntaxRule -let recover_syntax ntn = +let recover_notation_syntax ntn = try let prec = Notation.level_of_notation ntn in let pp_rule,_ = Notation.find_notation_printing_rule ntn in @@ -1271,29 +1262,25 @@ let recover_syntax ntn = raise NoSyntaxRule let recover_squash_syntax sy = - let sq = recover_syntax "{ _ }" in - [sy; sq] - -let recover_notation_syntax rawntn = - let ntn = contract_notation rawntn in - let sy = recover_syntax ntn in - let need_squash = not (String.equal ntn rawntn) in - let rules = if need_squash then recover_squash_syntax sy else [sy] in - sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting + let sq = recover_notation_syntax "{ _ }" in + sy :: sq.synext_notgram.notgram_rules (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule i_typs level (typs,symbols) ntn onlyprint = +let make_pa_rule level (typs,symbols) ntn need_squash = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - { notgram_level = level; + let sy = { + notgram_level = level; notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; - notgram_typs = i_typs; - notgram_onlyprinting = onlyprint; - } + } in + (* By construction, the rule for "{ _ }" is declared, but we need to + redeclare it because the file where it is declared needs not be open + when the current file opens (especially in presence of -nois) *) + if need_squash then recover_squash_syntax sy else [sy] let make_pp_rule level (typs,symbols) fmt = match fmt with @@ -1302,21 +1289,16 @@ let make_pp_rule level (typs,symbols) fmt = (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in - let ntn, prec, need_squash = sd.not_data in - let pa_rule = make_pa_rule sd.intern_typs sd.level sd.syntax_data ntn sd.only_printing in - let pp_rule = make_pp_rule sd.level sd.syntax_data sd.format in - let sy = { - synext_level = (sd.level, prec); - synext_notation = ntn; - synext_notgram = pa_rule; + let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in + let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in + let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in { + synext_level = sd.level; + synext_notation = fst sd.info; + synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; synext_unparsing = pp_rule; synext_extra = sd.extra; synext_compat = sd.compat; - } in - (* By construction, the rule for "{ _ }" is declared, but we need to - redeclare it because the file where it is declared needs not be open - when the current file opens (especially in presence of -nois) *) - if need_squash then recover_squash_syntax sy else [sy] + } (**********************************************************************) (* Main functions about notations *) @@ -1361,11 +1343,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin - let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in - let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in + let sy = recover_notation_syntax (make_notation_key symbs) in + let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (** If the only printing flag has been explicitly requested, put it back *) - let onlyprint = onlyprint || onlyprint' in - i_typs, onlyprint + let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in + pi3 sy.synext_level, onlyprint end else [], false in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in |