aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.circleci/config.yml4
-rw-r--r--.github/CODEOWNERS5
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--.merlin2
-rw-r--r--.travis.yml3
-rw-r--r--CHANGES1
-rw-r--r--META.coq13
-rw-r--r--Makefile.ci2
-rw-r--r--Makefile.common4
-rw-r--r--configure.ml2
-rw-r--r--dev/base_include1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-mtac2.sh (renamed from dev/ci/ci-metacoq.sh)6
-rw-r--r--dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh12
-rw-r--r--dev/core.dbg1
-rw-r--r--dev/doc/changes.md13
-rw-r--r--dev/doc/coq-src-description.txt6
-rw-r--r--dev/doc/debugging.md2
-rw-r--r--dev/ocamldebug-coq.run2
-rw-r--r--doc/sphinx/language/gallina-extensions.rst6
-rw-r--r--engine/engine.mllib1
-rw-r--r--engine/evar_kinds.ml (renamed from intf/evar_kinds.ml)0
-rw-r--r--engine/evarutil.ml46
-rw-r--r--engine/evarutil.mli23
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation_term.ml (renamed from intf/notation_term.ml)0
-rw-r--r--intf/intf.mllib11
-rw-r--r--library/decl_kinds.ml (renamed from intf/decl_kinds.ml)0
-rw-r--r--library/declaremods.ml16
-rw-r--r--library/declaremods.mli16
-rw-r--r--library/library.mllib2
-rw-r--r--library/misctypes.ml (renamed from intf/misctypes.ml)0
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--pretyping/constrexpr.ml (renamed from intf/constrexpr.ml)0
-rw-r--r--pretyping/extend.ml (renamed from intf/extend.ml)0
-rw-r--r--pretyping/genredexpr.ml (renamed from intf/genredexpr.ml)0
-rw-r--r--pretyping/glob_term.ml (renamed from intf/glob_term.ml)0
-rw-r--r--pretyping/locus.ml (renamed from intf/locus.ml)0
-rw-r--r--pretyping/pattern.ml (renamed from intf/pattern.ml)0
-rw-r--r--pretyping/pretyping.mllib9
-rw-r--r--pretyping/vernacexpr.ml (renamed from intf/vernacexpr.ml)12
-rw-r--r--printing/ppvernac.ml7
-rw-r--r--proofs/logic.ml68
-rw-r--r--tactics/tactics.ml52
-rw-r--r--test-suite/Makefile37
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comAssumption.ml3
-rw-r--r--vernac/comAssumption.mli4
-rw-r--r--vernac/vernacentries.ml2
50 files changed, 278 insertions, 132 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a55..d6a8e059c 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -207,6 +207,9 @@ jobs:
math-comp:
<<: *ci-template
+ mtac2:
+ <<: *ci-template
+
sf:
<<: *ci-template
environment:
@@ -251,6 +254,7 @@ workflows:
requires:
- build
- bignums
+ - mtac2: *req-main
- corn:
requires:
- build
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 029b55b9a..7f3ee5c37 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -86,11 +86,6 @@
/interp/ @herbelin
# Secondary maintainer @ejgallego
-########## Interfaces ##########
-
-/intf/ @letouzey
-# Secondary maintainer @ppedrot
-
########## Kernel ##########
/kernel/ @maximedenes
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d6b53964..e1c5b5255 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -360,6 +360,9 @@ ci-math-classes:
ci-math-comp:
<<: *ci-template
+ci-mtac2:
+ <<: *ci-template
+
ci-sf:
<<: *ci-template
variables:
diff --git a/.merlin b/.merlin
index d60f5037b..40db60950 100644
--- a/.merlin
+++ b/.merlin
@@ -10,8 +10,6 @@ S kernel
B kernel
S kernel/byterun
B kernel/byterun
-S intf
-B intf
S library
B library
S engine
diff --git a/.travis.yml b/.travis.yml
index fe376431e..052979bcb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -117,6 +117,9 @@ matrix:
- TEST_TARGET="ci-math-comp"
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="ci-mtac2"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-sf"
- if: NOT (type = pull_request)
env:
diff --git a/CHANGES b/CHANGES
index 502f848fb..2db8ace96 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,7 @@ Tactic language
- Ltac backtraces now include trace information about tactics
called by OCaml-defined tactics.
+- Option "Ltac Debug" now applies also to terms built using Ltac functions.
Changes from 8.8+beta1 to 8.8.0
===============================
diff --git a/META.coq b/META.coq
index 30bfdd67a..3414ccbd4 100644
--- a/META.coq
+++ b/META.coq
@@ -90,19 +90,6 @@ package "library" (
)
-package "intf" (
-
- description = "Coq Public Data Types"
- version = "8.8"
-
- requires = "coq.library"
-
- directory = "intf"
-
- archive(byte) = "intf.cma"
- archive(native) = "intf.cmxa"
-)
-
package "engine" (
description = "Coq Tactic Engine"
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f8723..37b14ed91 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,7 +28,7 @@ CI_TARGETS=ci-bignums \
ci-ltac2 \
ci-math-classes \
ci-math-comp \
- ci-metacoq \
+ ci-mtac2 \
ci-sf \
ci-tlc \
ci-unimath \
diff --git a/Makefile.common b/Makefile.common
index 9a30e2a4c..eed41fbe7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,7 +75,7 @@ INSTALLSH:=./install.sh
MKDIR:=install -d
CORESRCDIRS:=\
- config clib lib kernel intf kernel/byterun library \
+ config clib lib kernel kernel/byterun library \
engine pretyping interp proofs parsing printing \
tactics vernac stm toplevel
@@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
# respecting this order is useful for developers that want to load or link
# the libraries directly
-CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
+CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.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
diff --git a/configure.ml b/configure.ml
index d973f95e1..e77310eb7 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1222,7 +1222,7 @@ let write_configml f =
let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library";
"engine"; "pretyping"; "interp"; "parsing"; "proofs";
- "tactics"; "toplevel"; "printing"; "intf";
+ "tactics"; "toplevel"; "printing";
"grammar"; "ide"; "stm"; "vernac" ] in
let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n")
""
diff --git a/dev/base_include b/dev/base_include
index e76044f41..2f7183dd6 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,7 +15,6 @@
#directory "tactics";;
#directory "printing";;
#directory "grammar";;
-#directory "intf";;
#directory "stm";;
#directory "vernac";;
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a5117..5cee72cc7 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
########################################################################
: "${unicoq_CI_BRANCH:=master}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
########################################################################
# Mathclasses + Corn
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh
index a66dc1e76..1372acb8e 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
# Setup UniCoq
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
# Setup MetaCoq
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
new file mode 100644
index 000000000..7e554684e
--- /dev/null
+++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then
+
+ # Equations_CI_BRANCH=ssr+correct_packing
+ # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ # ltac2_CI_BRANCH=ssr+correct_packing
+ # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Elpi_CI_BRANCH=api+vernac_expr_iso
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/dev/core.dbg b/dev/core.dbg
index 57c136900..edf67020a 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,5 +16,4 @@ load_printer tactics.cma
load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
-load_printer intf.cma
load_printer ltac_plugin.cmo
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1a24f23e5..2bad21bb2 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,7 +5,18 @@
Proof engine
More functions have been changed to use `EConstr`, notably the
- functions in `Evd`.
+ functions in `Evd`, and in particular `Evd.define`.
+
+ Note that the core function `EConstr.to_constr` now _enforces_ by
+ default that the resulting term is ground, that is to say, free of
+ Evars. This is usually what you want, as open terms should be of
+ type `EConstr.t` to benefit from the invariants the `EConstr` API is
+ meant to guarantee.
+
+ In case you'd like to violate this API invariant, you can use the
+ `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+ that setting this flag to false is deprecated so it is only meant to
+ be used as to help port pre-EConstr code.
## Changes between Coq 8.7 and Coq 8.8
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e5..764d48295 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -17,12 +17,6 @@ toplevel
Special components
------------------
-intf :
-
- Contains mli-only interfaces, many of them providing a.s.t.
- used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
- produced by parsing and transformed by interp.
-
grammar :
Camlp5 syntax extensions. The file grammar/grammar.cma is used
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fd3cbd1bc..14a1cc693 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs
7. some hints:
- To debug a failure/error/anomaly, add a breakpoint in
- Vernac.vernac_com at the with clause of the "try ... interp com
+ `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
with ..." block, then go "back" a few steps to find where the
failure/error/anomaly has been raised
- Alternatively, for an error or an anomaly, add breakpoints in the middle
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f3e60edea..8f1c165dd 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -18,7 +18,7 @@ exec $OCAMLDEBUG \
-I $CAMLP5LIB -I +threads \
-I $COQTOP \
-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
- -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1a7628d89..a93e9b156 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any
Starts an interactive module satisfying each `module_type`.
- .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }.
+ .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }.
Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
is verified against each `module_type`.
@@ -1436,7 +1436,9 @@ For instance, the first argument of
in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A`
will always be inferable from the type :g:`list A` of the third argument of
-:g:`cons`. On the contrary, the second argument of a term of type
+:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one,
+since the first argument is exactly the type of the second argument.
+On the contrary, the second argument of a term of type
::
forall P:nat->Prop, forall n:nat, P n -> ex nat P
diff --git a/engine/engine.mllib b/engine/engine.mllib
index a3614f6c4..a5df5a9fa 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -2,6 +2,7 @@ Universes
Univops
UState
Nameops
+Evar_kinds
Evd
EConstr
Namegen
diff --git a/intf/evar_kinds.ml b/engine/evar_kinds.ml
index c964ecf1f..c964ecf1f 100644
--- a/intf/evar_kinds.ml
+++ b/engine/evar_kinds.ml
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 065b42bf6..710491f84 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -342,7 +342,15 @@ let update_var src tgt subst =
let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in
{ subst with csubst_var; csubst_rev }
-let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
+type naming_mode =
+ | KeepUserNameAndRenameExistingButSectionNames
+ | KeepUserNameAndRenameExistingEvenSectionNames
+ | KeepExistingNames
+ | FailIfConflict
+
+let push_rel_decl_to_named_context
+ ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
+ sigma decl (subst, avoid, nc) =
let open EConstr in
let open Vars in
let map_decl f d =
@@ -373,7 +381,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
in
match extract_if_neq id na with
- | Some id0 when not (is_section_variable id0) ->
+ | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames ||
+ hypnaming = KeepUserNameAndRenameExistingButSectionNames &&
+ not (is_section_variable id0) ->
(* spiwack: if [id<>id0], rather than introducing a new
binding named [id], we will keep [id0] (the name given
by the user) and rename [id0] into [id] in the named
@@ -382,6 +392,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
let nc = List.map (replace_var_named_declaration id0 id) nc in
(push_var id0 subst, Id.Set.add id avoid, d :: nc)
+ | Some id0 when hypnaming = FailIfConflict ->
+ user_err Pp.(Id.print id0 ++ str " is already used.")
| _ ->
(* spiwack: if [id0] is a section variable renaming it is
incorrect. We revert to a less robust behaviour where
@@ -390,7 +402,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) =
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
(push_var id subst, Id.Set.add id avoid, d :: nc)
-let push_rel_context_to_named_context env sigma typ =
+let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* compute the instances relative to the named context and rel_context *)
let open Context.Named.Declaration in
let open EConstr in
@@ -405,7 +417,7 @@ let push_rel_context_to_named_context env sigma typ =
(* with vars of the rel context *)
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, _, env) =
- Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+ Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc)
(rel_context env) ~init:(empty_csubst, avoid, named_context env) in
(val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
@@ -468,8 +480,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin
(* [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 =
- let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ =
+ let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
let map c = csubst_subst subst c in
let candidates = Option.map (fun l -> List.map map l) candidates in
let instance =
@@ -478,13 +490,13 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
| Some filter -> Filter.filter_list filter instance in
new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
-let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
+let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid =
let (evd', s) = new_sort_variable rigid evd in
- let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in
+ let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
evd', (e, s)
-let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
- let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
+let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid =
+ let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in
evdref := evd;
c
@@ -498,8 +510,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
evdref := evd'; EConstr.mkSort s
(* The same using side-effect *)
-let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
- let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty =
+ let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in
evdref := evd';
ev
@@ -522,7 +534,7 @@ type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of existential
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
exception Depends of Id.t
@@ -533,13 +545,13 @@ let rec check_and_clear_in_constr env evdref err ids global c =
is a section variable *)
match kind c with
| Var id' ->
- if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
+ if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c
| ( Const _ | Ind _ | Construct _ ) ->
let () = if global then
let check id' =
if Id.Set.mem id' ids then
- raise (ClearDependencyError (id',err))
+ raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
in
Id.Set.iter check (Environ.vars_of_global env c)
in
@@ -587,8 +599,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
let global = Id.Set.exists is_section_variable nids in
let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl
- with ClearDependencyError (rid,err) ->
- raise (ClearDependencyError (Id.Map.find rid rids,err)) in
+ with ClearDependencyError (rid,err,where) ->
+ raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in
if Id.Map.is_empty rids then c
else
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 40c1ee082..d3937f28e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -30,11 +30,17 @@ val new_evar_from_context :
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> evar_map * EConstr.t
+type naming_mode =
+ | KeepUserNameAndRenameExistingButSectionNames
+ | KeepUserNameAndRenameExistingEvenSectionNames
+ | KeepExistingNames
+ | FailIfConflict
+
val new_evar :
env -> 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
+ ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t
val new_pure_evar :
named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
@@ -49,18 +55,20 @@ val e_new_evar :
env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> types -> constr
+ ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
+ ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?principal:bool -> ?hypnaming:naming_mode -> rigid ->
evar_map * (constr * Sorts.t)
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t
+ ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
@@ -224,7 +232,7 @@ type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of Constr.existential
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
Id.Set.t -> named_context_val * types
@@ -240,10 +248,11 @@ val csubst_subst : csubst -> constr -> constr
type ext_named_context =
csubst * Id.Set.t * named_context
-val push_rel_decl_to_named_context :
+val push_rel_decl_to_named_context : ?hypnaming:naming_mode ->
evar_map -> rel_declaration -> ext_named_context -> ext_named_context
-val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
+val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
+ Environ.env -> evar_map -> types ->
named_context_val * types * constr list * csubst
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf468..61313acc4 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,7 @@
Tactypes
Stdarg
Genintern
+Notation_term
Notation_ops
Notation
Syntax_def
diff --git a/intf/notation_term.ml b/interp/notation_term.ml
index a9c2e2a53..a9c2e2a53 100644
--- a/intf/notation_term.ml
+++ b/interp/notation_term.ml
diff --git a/intf/intf.mllib b/intf/intf.mllib
deleted file mode 100644
index 2b8960d3f..000000000
--- a/intf/intf.mllib
+++ /dev/null
@@ -1,11 +0,0 @@
-Constrexpr
-Evar_kinds
-Genredexpr
-Locus
-Extend
-Notation_term
-Decl_kinds
-Glob_term
-Misctypes
-Pattern
-Vernacexpr
diff --git a/intf/decl_kinds.ml b/library/decl_kinds.ml
index 0d3285311..0d3285311 100644
--- a/intf/decl_kinds.ml
+++ b/library/decl_kinds.ml
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 762efc5e3..1d5df49cf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,11 +17,25 @@ open Entries
open Libnames
open Libobject
open Mod_subst
-open Vernacexpr
open Misctypes
(** {6 Inlining levels} *)
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+ | Enforce of 'a (** ... : T *)
+ | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+ either None or the ones whose level is less or equal
+ to the given integer *)
+
+type inline =
+ | NoInline
+ | DefaultInline
+ | InlineAt of int
+
let default_inline () = Some (Flags.get_inline_level ())
let inl2intopt = function
diff --git a/library/declaremods.mli b/library/declaremods.mli
index fd8d29614..4aee7feae 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -9,10 +9,24 @@
(************************************************************************)
open Names
-open Vernacexpr
(** {6 Modules } *)
+(** Rigid / flexible module signature *)
+
+type 'a module_signature =
+ | Enforce of 'a (** ... : T *)
+ | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Which module inline annotations should we honor,
+ either None or the ones whose level is less or equal
+ to the given integer *)
+
+type inline =
+ | NoInline
+ | DefaultInline
+ | InlineAt of int
+
type 'modast module_interpretor =
Environ.env -> Misctypes.module_kind -> 'modast ->
Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
diff --git a/library/library.mllib b/library/library.mllib
index e43bfb5a1..1c0368847 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -4,7 +4,9 @@ Libobject
Summary
Nametab
Global
+Decl_kinds
Lib
+Misctypes
Declaremods
Loadpath
Library
diff --git a/intf/misctypes.ml b/library/misctypes.ml
index 72db3b31c..72db3b31c 100644
--- a/intf/misctypes.ml
+++ b/library/misctypes.ml
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 593dcbf58..2dbd624c2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -17,6 +17,7 @@ open Constrexpr
open Constrexpr_ops
open Extend
open Decl_kinds
+open Declaremods
open Declarations
open Misctypes
open Tok (* necessary for camlp5 *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6a4bf577b..84049d4ed 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2010,7 +2010,8 @@ let interp_redexp env sigma r =
let _ =
let eval lfun env sigma ty tac =
- let ist = { lfun = lfun; extra = TacStore.empty; } in
+ let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
+ let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
diff --git a/intf/constrexpr.ml b/pretyping/constrexpr.ml
index fda31756a..fda31756a 100644
--- a/intf/constrexpr.ml
+++ b/pretyping/constrexpr.ml
diff --git a/intf/extend.ml b/pretyping/extend.ml
index 734b859f6..734b859f6 100644
--- a/intf/extend.ml
+++ b/pretyping/extend.ml
diff --git a/intf/genredexpr.ml b/pretyping/genredexpr.ml
index 80697461a..80697461a 100644
--- a/intf/genredexpr.ml
+++ b/pretyping/genredexpr.ml
diff --git a/intf/glob_term.ml b/pretyping/glob_term.ml
index 84be15552..84be15552 100644
--- a/intf/glob_term.ml
+++ b/pretyping/glob_term.ml
diff --git a/intf/locus.ml b/pretyping/locus.ml
index 95a2e495b..95a2e495b 100644
--- a/intf/locus.ml
+++ b/pretyping/locus.ml
diff --git a/intf/pattern.ml b/pretyping/pattern.ml
index 76367b612..76367b612 100644
--- a/intf/pattern.ml
+++ b/pretyping/pattern.ml
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ae4ad0be7..d98026bc6 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,5 +1,5 @@
Geninterp
-Ltac_pretype
+Locus
Locusops
Pretype_errors
Reductionops
@@ -16,12 +16,19 @@ Evarsolve
Recordops
Evarconv
Typing
+Constrexpr
+Genredexpr
Miscops
+Glob_term
+Ltac_pretype
Glob_ops
Redops
+Pattern
Patternops
Constr_matching
Tacred
+Extend
+Vernacexpr
Typeclasses_errors
Typeclasses
Classops
diff --git a/intf/vernacexpr.ml b/pretyping/vernacexpr.ml
index 06f969f19..4e1c986f1 100644
--- a/intf/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -281,20 +281,22 @@ type bullet =
(** Rigid / flexible module signature *)
-type 'a module_signature =
+type 'a module_signature = 'a Declaremods.module_signature =
| Enforce of 'a (** ... : T *)
| Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
(** Which module inline annotations should we honor,
either None or the ones whose level is less or equal
to the given integer *)
-type inline =
+type inline = Declaremods.inline =
| NoInline
| DefaultInline
| InlineAt of int
+[@@ocaml.deprecated "please use [Declaremods.inline]."]
-type module_ast_inl = module_ast * inline
+type module_ast_inl = module_ast * Declaremods.inline
type module_binder = bool option * lident list * module_ast_inl
(** [Some b] if locally enabled/disabled according to [b], [None] if
@@ -333,7 +335,7 @@ type nonrec vernac_expr =
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
- inline * (ident_decl list * constr_expr) with_coercion list
+ Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
| VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
@@ -373,7 +375,7 @@ type nonrec vernac_expr =
| VernacDeclareModule of bool option * lident *
module_binder list * module_ast_inl
| VernacDefineModule of bool option * lident * module_binder list *
- module_ast_inl module_signature * module_ast_inl list
+ module_ast_inl Declaremods.module_signature * module_ast_inl list
| VernacDeclareModuleType of lident *
module_binder list * module_ast_inl list * module_ast_inl list
| VernacInclude of module_ast_inl list
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7eb8396ac..83c875707 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -16,12 +16,13 @@ open Util
open CAst
open Extend
-open Vernacexpr
-open Pputils
open Libnames
+open Decl_kinds
open Constrexpr
open Constrexpr_ops
-open Decl_kinds
+open Vernacexpr
+open Declaremods
+open Pputils
open Ppconstr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e5294715e..4934afa83 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -289,7 +289,15 @@ let collect_meta_variables c =
let rec collrec deep acc c = match kind c with
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
- | (App _| Case _) -> Constr.fold (collrec deep) acc c
+ | Case(ci,p,c,br) ->
+ (* Hack assuming only two situations: the legacy one that branches,
+ if with Metas, are Meta, and the new one with eta-let-expanded
+ branches *)
+ let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
+ Array.fold_left (collrec deep)
+ (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c)
+ br
+ | App _ -> Constr.fold (collrec deep) acc c
| Proj (_, c) -> collrec deep acc c
| _ -> Constr.fold (collrec true) acc c
in
@@ -387,12 +395,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| Case (ci,p,c,lf) ->
let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
- let (acc'',sigma, rbranches) =
- Array.fold_left2
- (fun (lacc,sigma,bacc) ty fi ->
- let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
- (acc',sigma,[]) lbrty lf
- in
+ let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -440,12 +443,7 @@ and mk_hdgoals sigma goal goalacc trm =
| Case (ci,p,c,lf) ->
let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
- let (acc'',sigma,rbranches) =
- Array.fold_left2
- (fun (lacc,sigma,bacc) ty fi ->
- let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc))
- (acc',sigma,[]) lbrty lf
- in
+ let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -497,6 +495,50 @@ and mk_casegoals sigma goal goalacc p c =
let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
(acc'',lbrty,conclty,sigma,p',c')
+and treat_case sigma goal ci lbrty lf acc' =
+ let rec strip_outer_cast c = match kind c with
+ | Cast (c,_,_) -> strip_outer_cast c
+ | _ -> c in
+ let decompose_app_vect c = match kind c with
+ | App (f,cl) -> (f, cl)
+ | _ -> (c,[||]) in
+ let env = Goal.V82.env sigma goal in
+ Array.fold_left3
+ (fun (lacc,sigma,bacc) ty fi l ->
+ if isMeta (strip_outer_cast fi) then
+ (* Support for non-eta-let-expanded Meta as found in *)
+ (* destruct/case with an non eta-let expanded elimination scheme *)
+ let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+ r,s,(fi'::bacc)
+ else
+ (* Deal with a branch in expanded form of the form
+ Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as
+ if it were not so, so as to preserve compatibility with when
+ destruct/case generated schemes of the form
+ Case(ci,p,c,[|Meta;...;Meta|];
+ CAUTION: it does not deal with the general case of eta-zeta
+ reduced branches having a form different from Meta, as it
+ would be theoretically the case with third-party code *)
+ let n = List.length l in
+ let ctx, body = Term.decompose_lam_n_decls n fi in
+ let head, args = decompose_app_vect body in
+ (* Strip cast because clenv_cast_meta adds a cast when the branch is
+ eta-expanded but when not when the branch has the single-meta
+ form [Meta] *)
+ let head = strip_outer_cast head in
+ if isMeta head then begin
+ assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
+ let head' = lift (-n) head in
+ let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+ let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
+ (r,s,fi'::bacc)
+ end
+ else
+ (* Supposed to be meta-free *)
+ let sigma, t'ty = goal_type_of env sigma fi in
+ let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+ (lacc,sigma,fi::bacc))
+ (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
let convert_hyp check sign sigma d =
let id = NamedDecl.get_id d in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc088..c6d262fef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -198,32 +198,40 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -242,7 +250,7 @@ let clear_gen fail = function
let evdref = ref sigma in
let (hyps, concl) =
try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
@@ -426,8 +434,8 @@ 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)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -3007,8 +3015,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8239600b1..9d84cd5c7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -79,6 +79,8 @@ log_anomaly = "==========> FAILURE <=========="
log_failure = "==========> FAILURE <=========="
log_intro = "==========> TESTING $(1) <=========="
+FAIL = >&2 echo 'FAILED $@'
+
#######################################################################
# Testing subsystems
#######################################################################
@@ -115,25 +117,24 @@ run: $(SUBSYSTEMS)
bugs: $(BUGS)
clean:
- rm -f trace .lia.cache
- $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
+ rm -f trace .lia.cache output/MExtraction.out
+ $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>"
$(HIDE)find . \( \
- -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
+ -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
\) -print0 | xargs -0 rm -f
distclean: clean
- $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f
+ $(SHOW) "RM <**/*.aux>"
+ $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f
#######################################################################
# Per-subsystem targets
#######################################################################
-define mkstamp
-$(1): $(1).stamp ; @true
-$(1).stamp: $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) ; \
- $(HIDE)touch $$@
+define vdeps
+$(1): $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v))
endef
-$(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))))
+$(foreach S,$(VSUBSYSTEMS),$(eval $(call vdeps,$(S))))
#######################################################################
# Summary
@@ -221,6 +222,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
else \
echo $(log_failure); \
echo " $<...Error! (bug seems to be closed, please check)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -236,6 +238,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
else \
echo $(log_failure); \
echo " $<...Error! (bug seems to be opened, please check)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -251,6 +254,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be prepared" ; \
+ $(FAIL); \
else \
echo $(log_success); \
echo " $<...correctly prepared" ; \
@@ -269,6 +273,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
else \
echo $(log_failure); \
echo " $<...Error! (should be accepted)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -285,6 +290,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
else \
echo $(log_failure); \
echo " $<...Error! (should be accepted)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -299,6 +305,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
else \
echo $(log_failure); \
echo " $<...Error! (should be rejected)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -321,6 +328,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
else \
echo $(log_failure); \
echo " $<...Error! (unexpected output)"; \
+ $(FAIL); \
fi; \
rm $$tmpoutput; \
} > "$@"
@@ -363,6 +371,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
else \
echo $(log_failure); \
echo " $<...Error! (unexpected output)"; \
+ $(FAIL); \
fi; \
rm $$tmpoutput; \
rm $$tmpexpected; \
@@ -379,6 +388,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
else \
echo $(log_failure); \
echo " $<...Error! (should be accepted)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -411,6 +421,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
else \
echo $(log_failure); \
echo " $<...Error! (should run faster)"; \
+ $(FAIL); \
fi; \
fi; \
} > "$@"
@@ -428,6 +439,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
else \
echo $(log_failure); \
echo " $<...Good news! (wish seems to be granted, please check)"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -462,6 +474,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
else \
echo $(log_failure); \
echo " $<...Error!"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -480,6 +493,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
else \
echo $(log_failure); \
echo " $<...Error!"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -499,6 +513,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
else \
echo $(log_failure); \
echo " $<...Error!"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -517,6 +532,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
else \
echo $(log_failure); \
echo " $<...Error!"; \
+ $(FAIL); \
fi; \
} > "$@"
@@ -536,6 +552,7 @@ coqwc/%.v.log : coqwc/%.v
else \
echo $(log_failure); \
echo " $<...Error! (unexpected output)"; \
+ $(FAIL); \
fi; \
rm $$tmpoutput; \
} > "$@"
@@ -556,6 +573,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh
else \
echo $(log_failure); \
echo " $<...Error!"; \
+ $(FAIL); \
fi; \
) > "$@"
@@ -580,5 +598,6 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR
else \
echo $(log_failure); \
echo " $<...Error! (unexpected output)"; \
+ $(FAIL); \
fi; \
} > "$@"
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3c133f317..7f2642093 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -425,7 +425,7 @@ let context poly l =
let nstatus = match b with
| None ->
pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
- Vernacexpr.NoInline (CAst.make id))
+ Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 6a590758f..26a46a752 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -20,7 +20,6 @@ open Constrintern
open Impargs
open Decl_kinds
open Pretyping
-open Vernacexpr
open Entries
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -66,7 +65,7 @@ match local with
| Global | Local | Discharge ->
let do_instance = should_axiom_into_instance local in
let local = DeclareDef.get_locality ident ~kind:"axiom" local in
- let inl = match nl with
+ let inl = let open Declaremods in match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 56e324376..a2d20a1d1 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -19,7 +19,7 @@ open Decl_kinds
(** {6 Parameters/Assumptions} *)
val do_assumptions : locality * polymorphic * assumption_object_kind ->
- Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
+ Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
(************************************************************************)
(** Internal API *)
@@ -32,5 +32,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
+ bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
global_reference * Univ.Instance.t * bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a9d1631ba..19658806c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module Modintern.interp_module_ast
- id binders_ast (Enforce mty_ast) []
+ id binders_ast (Declaremods.Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:49:47 +0000