diff options
96 files changed, 1130 insertions, 727 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 274a0001b1..d9136ee24b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,11 +6,23 @@ /.github/ @maximedenes # Secondary maintainer @Zimmi48 +########## Build system ########## + +/Makefile* @gares + +/configure* @ejgallego + +/META.coq.in @ejgallego + +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests @@ -21,8 +33,7 @@ /dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer -/default.nix @Zimmi48 -# Secondary maintainer @vbgl +*.nix @coq/nix-maintainers ########## Documentation ########## @@ -43,6 +54,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -302,25 +314,6 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes -########## Build system ########## - -/Makefile* @gares - -/configure* @ejgallego - -/META.coq.in @ejgallego - -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes - -# This file belongs to CI -/Makefile.ci @ejgallego -# Secondary maintainer @SkySkimmer - -# This file belongs to the doc -/Makefile.doc @maximedenes -# Secondary maintainer @silene - ########## Test suite ########## /test-suite/Makefile @gares @@ -10,6 +10,11 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). +- New command "Declare Scope" to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is + deprecated. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -34,6 +39,10 @@ Tactics - Deprecated the Implicit Tactic family of commands. +- The default program obligation tactic uses a bounded proof search + instead of an unbounded and potentially non-terminating one now + (source of incompatibility). + - The `simple apply` tactic now respects the `Opaque` flag when called from Ltac (`auto` still does not respect it). @@ -48,6 +57,8 @@ Tactics may need to add `Require Import Lra` to your developments. For compatibility, we now define `fourier` as a deprecated alias of `lra`. +- The `romega` tactics have been deprecated; please use `lia` instead. + Focusing - Focusing bracket `{` now supports named goal selectors, @@ -177,6 +177,9 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### camldevfiles: $(MERLINFILES) META.coq +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + .merlin: .merlin.in cp -a "$<" "$@" diff --git a/default.nix b/default.nix index 80dca47f69..6f759f41d1 100644 --- a/default.nix +++ b/default.nix @@ -75,7 +75,7 @@ stdenv.mkDerivation rec { ++ [ ocamlPackages.ounit rsync which ] ) ++ optionals shell ( - [ jq curl git gnupg ] # Dependencies of the merging script + [ jq curl gitFull gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools ); diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh new file mode 100644 index 0000000000..3a6480a5a1 --- /dev/null +++ b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then + + ltac2_CI_BRANCH=master+globenv-coq-pr7288 + ltac2_CI_GITURL=https://github.com/herbelin/ltac2 + +fi diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c0c4539564..23cbd76eda 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -325,6 +325,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1e92d01125..f7a431ef29 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,7 +26,9 @@ Description of ``omega`` .. tacv:: romega :name: romega - To be documented. + .. deprecated:: 8.9 + + Use :tacn:`lia` instead. Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index b46382dbbf..4c0e85bdd4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See :ref:`above <NotationSyntax>` for the syntax of notations including the -possibility to declare them in a given scope. Here is a typical example which -declares the notation for conjunction in the scope ``type_scope``. +.. cmd:: Declare Scope @scope + + This adds a new scope named :n:`@scope`. Note that the initial + state of Coq declares by default the following interpretation scopes: + ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, + ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. + +The syntax to associate a notation to a scope is given +:ref:`above <NotationSyntax>`. Here is a typical example which declares the +notation for conjunction in the scope ``type_scope``. .. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. .. note:: A notation not defined in a scope is called a *lonely* - notation. + notation. No example of lonely notations can be found in the + initial state of Coq though. + Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely interpretations and opening of scopes matters, and not the declaration of interpretations within a scope). -The initial state of Coq declares three interpretation scopes and no -lonely notations. These scopes, in opening order, are ``core_scope``, -``type_scope`` and ``nat_scope``. - .. cmd:: Open Scope @scope The command to add a scope to the interpretation scope stack is diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b77bf55d8d..b1d880b0ad 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -284,8 +284,8 @@ type csubst = { csubst_rev : subst_val Id.Map.t; (** Reverse mapping of the substitution *) } -(** This type represent a name substitution for the named and De Bruijn parts of - a environment. For efficiency we also store the reverse substitution. +(** This type represents a name substitution for the named and De Bruijn parts of + an environment. For efficiency we also store the reverse substitution. Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel] must be pairwise distinct. *) diff --git a/interp/notation.ml b/interp/notation.ml index 55ead946cb..6b26f66100 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -98,21 +98,40 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) +let warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") + let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope + +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () + +let ensure_scope scope = check_scope ~tolerant:true scope -let check_scope sc = let _ = find_scope sc in () +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -418,7 +437,7 @@ type prim_token_infos = { let cache_prim_token_interpretation (_,infos) = let sc = infos.pt_scope in let uid = infos.pt_uid in - declare_scope sc; + check_scope ~tolerant:true sc; prim_token_interp_infos := String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := diff --git a/interp/notation.mli b/interp/notation.mli index e5478eff48..6e59c0fd70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *) val declare_scope : scope_name -> unit +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit + val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7c00e40fb0..961036d3c5 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -269,7 +269,7 @@ let lam_subst_args subst args = let can_subst lam = match lam with | Lrel _ | Lvar _ | Lconst _ - | Lval _ | Lsort _ | Lind _ | Llam _ -> true + | Lval _ | Lsort _ | Lind _ -> true | _ -> false let rec simplify subst lam = diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4a2..f1095fc9f1 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,13 +417,13 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega end. Hint Resolve Pos.le_max_r Pos.le_max_l. @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a0446bd6a0..f4313a8fa3 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2029,7 +2029,7 @@ let _ = let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in (EConstr.of_constr c, sigma) in - Pretyping.register_constr_interp0 wit_tactic eval + GlobEnv.register_constr_interp0 wit_tactic eval let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 51b99b9935..da86f4274d 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -8,6 +8,7 @@ *************************************************************************) Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. +Declare Scope Int_scope. Delimit Scope Int_scope with I. (** * Abstract Integers. *) @@ -716,6 +717,7 @@ Inductive term : Set := | Topp : term -> term | Tvar : N -> term. +Declare Scope romega_scope. Bind Scope romega_scope with term. Delimit Scope romega_scope with term. Arguments Tint _%I. diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg index c1ce30027e..ac4f30b1db 100644 --- a/plugins/romega/g_romega.mlg +++ b/plugins/romega/g_romega.mlg @@ -41,14 +41,22 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +let romega_depr = + Vernacinterp.mk_deprecation + ~since:(Some "8.9") + ~note:(Some "Use lia instead.") + () + } TACTIC EXTEND romega +DEPRECATED { romega_depr } | [ "romega" ] -> { romega_tactic false [] } | [ "unsafe_romega" ] -> { romega_tactic true [] } END TACTIC EXTEND romega' +DEPRECATED { romega_depr } | [ "romega" "with" ne_ident_list(l) ] -> { romega_tactic false (List.map Names.Id.to_string l) } | [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index d9e32dbbf8..ce115f564f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -19,6 +19,7 @@ Section MakeFieldPol. (* Field elements : R *) Variable R:Type. +Declare Scope R_scope. Bind Scope R_scope with R. Delimit Scope R_scope with ring. Local Open Scope R_scope. @@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth. (* Coefficients : C *) Variable C: Type. +Declare Scope C_scope. Bind Scope C_scope with C. Delimit Scope C_scope with coef. @@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). (* Polynomial expressions : (PExpr C) *) +Declare Scope PE_scope. Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index fbe3b000fb..602fcfcab5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -293,7 +293,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let c, cl, ucst = match_pat env p occ h cl in let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in - let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in + let gl = try pf_unify_HO gl inf_t c + with exn when CErrors.noncritical exn -> error gl c inf_t in cl, gl, post with | NoMatch | NoProgress -> @@ -302,7 +303,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let e = EConstr.of_constr e in let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in let e, _, _, gl = pf_saturate ~beta:true gl e n in - let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in + let gl = try pf_unify_HO gl inf_t e + with exn when CErrors.noncritical exn -> error gl e inf_t in cl, gl, post in let rec match_all concl gl patterns = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 23cbf49c05..f23433f2f4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -115,7 +115,8 @@ let newssrcongrtac arg ist gl = (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = - match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with + match try Some (pf_unify_HO gl_c (pf_concl gl) c) + with exn when CErrors.noncritical exn -> None with | Some gl_c -> tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) (t_ok (proj gl_c)) gl diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 30a998c6ce..20ea8b3667 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -291,7 +291,10 @@ let unif_EQ_args env sigma pa a = prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a ;; -let unif_HO env ise p c = Evarconv.the_conv_x env p c ise +let unif_HO env ise p c = + try Evarconv.the_conv_x env p c ise + with Evarconv.UnableToUnify(ise, err) -> + raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) let unif_HO_args env ise0 pa i ca = let n = Array.length pa in diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + (* Notation to define shortcuts for the "X in t" part of a pattern. *) Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ad33297f0a..7baa755ab5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -35,7 +35,7 @@ open Evarsolve open Evarconv open Evd open Context.Rel.Declaration -open Ltac_pretype +open GlobEnv module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -114,8 +114,10 @@ let rec relocate_index sigma n1 n2 k t = (**********************************************************************) (* Structures used in compiling pattern-matching *) +let (!!) env = GlobEnv.env env + type 'a rhs = - { rhs_env : env; + { rhs_env : GlobEnv.t; rhs_vars : Id.Set.t; avoid_ids : Id.Set.t; it : 'a option} @@ -247,8 +249,7 @@ let push_history_pattern n pci cont = *) type 'a pattern_matching_problem = - { env : env; - lvar : Ltac_pretype.ltac_var_map; + { env : GlobEnv.t; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -256,7 +257,7 @@ type 'a pattern_matching_problem = mat : 'a matrix; caseloc : Loc.t option; casestyle : case_style; - typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } + typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment } (*--------------------------------------------------------------------------* * A few functions to infer the inductive type from the patterns instead of * @@ -331,6 +332,10 @@ let binding_vars_of_inductive sigma = function | NotInd _ -> [] | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs +let set_tomatch_realnames names = function + | NotInd _ as t -> t + | IsInd (typ,ind,_) -> IsInd (typ,ind,names) + let extract_inductive_data env sigma decl = match decl with | LocalAssum (_,t) -> @@ -357,58 +362,58 @@ let find_tomatch_tycon evdref env loc = function | None -> empty_tycon,None -let make_return_predicate_ltac_lvar sigma na tm c lvar = +let make_return_predicate_ltac_lvar env sigma na tm c = + (* If we have an [x as x return ...] clause and [x] expands to [c], + we have to update the status of [x] in the substitution: + - if [c] is a variable [id'], then [x] should now become [id'] + - otherwise, [x] should be hidden *) match na, DAst.get tm with | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> - if Id.Map.mem id lvar.ltac_genargs then - let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in - let ltac_idents = match kind sigma c with - | Var id' -> Id.Map.add id id' lvar.ltac_idents - | _ -> lvar.ltac_idents in - { lvar with ltac_genargs; ltac_idents } - else lvar - | _ -> lvar - -let ltac_interp_realnames lvar = function - | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) - | _ as x -> x + let expansion = match kind sigma c with + | Var id' -> Name id' + | _ -> Anonymous in + GlobEnv.hide_variable env expansion id + | _ -> env let is_patvar pat = match DAst.get pat with | PatVar _ -> true | _ -> false -let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = +let coerce_row typing_fun evdref env pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in - let tycon,realnames = find_tomatch_tycon evdref env loc indopt in - let j = typing_fun tycon env evdref !lvar tomatch in - let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in + let tycon,realnames = find_tomatch_tycon evdref !!env loc indopt in + let j = typing_fun tycon env evdref tomatch in + let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env) evdref j in let typ = nf_evar !evdref j.uj_type in - lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; + let env = make_return_predicate_ltac_lvar env !evdref na tomatch j.uj_val in let t = if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else - try try_find_ind env !evdref typ realnames + try try_find_ind !!env !evdref typ realnames with Not_found -> - unify_tomatch_with_patterns evdref env loc typ pats realnames in - (j.uj_val,t) + unify_tomatch_with_patterns evdref !!env loc typ pats realnames in + (env,(j.uj_val,t)) -let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = +let coerce_to_indtype typing_fun evdref env matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) | m -> m in - let lvar = ref lvar in - let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in - let tms = List.map (ltac_interp_realnames !lvar) tms in - !lvar,tms + let env,tms = List.fold_left2_map (fun env -> coerce_row typing_fun evdref env) env matx' tomatchl in + env,tms (************************************************************************) (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in e +let evd_comb2 f evdref x y = + let (evd',y) = f !evdref x y in + evdref := evd'; + y + let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the term to match and the patterns coerce *) @@ -418,7 +423,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let typ,names = match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in let tmtyp = - try try_find_ind pb.env !(pb.evdref) typ names + try try_find_ind !!(pb.env) !(pb.evdref) typ names with Not_found -> NotInd (None,typ) in match tmtyp with | NotInd (None,typ) -> @@ -426,17 +431,17 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (match find_row_ind tm1 with | None -> (current,tmtyp) | Some (_,(ind,_)) -> - let indt = inductive_template pb.evdref pb.env None ind in + let indt = inductive_template pb.evdref !!(pb.env) None ind in let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in + let () = Option.iter ((:=) pb.evdref) (cumul !!(pb.env) !(pb.evdref) indt typ) in current else - (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to true !!(pb.env)) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in - (current,try_find_ind pb.env sigma indt names)) + (current,try_find_ind !!(pb.env) sigma indt names)) | _ -> (current,tmtyp) let type_of_tomatch = function @@ -466,10 +471,10 @@ let remove_current_pattern eqn = alias_stack = alias_of_pat pat :: eqn.alias_stack } | [] -> anomaly (Pp.str "Empty list of patterns.") -let push_current_pattern (cur,ty) eqn = +let push_current_pattern sigma (cur,ty) eqn = match eqn.patterns with | pat::pats -> - let rhs_env = push_rel (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in + let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -739,7 +744,7 @@ let merge_name get_name obj = function let merge_names get_name = List.map2 (merge_name get_name) -let get_names env sigma sign eqns = +let get_names avoid env sigma sign eqns = let names1 = List.make (Context.Rel.length sign) Anonymous in (* If any, we prefer names used in pats, from top to bottom *) let names2,aliasname = @@ -752,7 +757,7 @@ let get_names env sigma sign eqns = avoiding conflicts with user ids *) let allvars = List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids) - Id.Set.empty eqns in + avoid eqns in let names3,_ = List.fold_left2 (fun (l,avoid) d na -> @@ -774,7 +779,7 @@ let get_names env sigma sign eqns = let recover_initial_subpattern_names = List.map2 RelDecl.set_name -let recover_and_adjust_alias_names names sign = +let recover_and_adjust_alias_names (_,avoid) names sign = let rec aux = function | [],[] -> [] @@ -786,31 +791,31 @@ let recover_and_adjust_alias_names names sign = in List.split (aux (names,sign)) -let push_rels_eqn sign eqn = +let push_rels_eqn sigma sign eqn = {eqn with - rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} } + rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } } -let push_rels_eqn_with_names sign eqn = +let push_rels_eqn_with_names sigma sign eqn = let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in let subpatnames = List.map alias_of_pat subpats in let sign = recover_initial_subpattern_names subpatnames sign in - push_rels_eqn sign eqn + push_rels_eqn sigma sign eqn -let push_generalized_decl_eqn env n decl eqn = +let push_generalized_decl_eqn env sigma n decl eqn = match RelDecl.get_name decl with | Anonymous -> - push_rels_eqn [decl] eqn + push_rels_eqn sigma [decl] eqn | Name _ -> - push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn + push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn let drop_alias_eqn eqn = { eqn with alias_stack = List.tl eqn.alias_stack } -let push_alias_eqn alias eqn = +let push_alias_eqn sigma alias eqn = let aliasname = List.hd eqn.alias_stack in let eqn = drop_alias_eqn eqn in let alias = RelDecl.set_name aliasname alias in - push_rels_eqn [alias] eqn + push_rels_eqn sigma [alias] eqn (**********************************************************************) (* Functions to deal with elimination predicate *) @@ -958,7 +963,7 @@ let rec extract_predicate ccl = function ccl let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = - let sign = make_arity_signature env sigma true indf in + let sign = make_arity_signature !!env sigma true indf in (* n is the number of real args + 1 (+ possible let-ins in sign) *) let n = List.length sign in (* Before abstracting we generalize over cur and on those realargs *) @@ -979,7 +984,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let pred = extract_predicate ccl tms in (* Build the predicate properly speaking *) let sign = List.map2 set_name (na::names) sign in - it_mkLambda_or_LetIn_name env sigma pred sign + it_mkLambda_or_LetIn_name !!env sigma pred sign (* [expand_arg] is used by [specialize_predicate] if Yk denotes [Xk;xk] or [Xk], @@ -1208,7 +1213,7 @@ let first_clause_irrefutable env = function let group_equations pb ind current cstrs mat = let mat = - if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in + if first_clause_irrefutable !!(pb.env) mat then [List.hd mat] else mat in let brs = Array.make (Array.length cstrs) [] in let only_default = ref None in let _ = @@ -1216,7 +1221,7 @@ let group_equations pb ind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with + match DAst.get (check_and_adjust_constructor !!(pb.env) ind cstrs pat) with | PatVar name -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do @@ -1238,7 +1243,7 @@ let rec generalize_problem names pb = function | [] -> pb, [] | i::l -> let pb',deps = generalize_problem names pb l in - let d = map_constr (lift i) (lookup_rel i pb.env) in + let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in begin match d with | LocalDef (Anonymous,_,_) -> pb', deps | _ -> @@ -1271,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* that had matched constructor C *) let cs_args = const_info.cs_args in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in - let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in + let names,aliasname = get_names (GlobEnv.vars_of_env pb.env) !!(pb.env) !(pb.evdref) cs_args eqns in let typs = List.map2 RelDecl.set_name names cs_args in @@ -1279,7 +1284,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* This is a bit too strong I think, in the sense that what we would *) (* really like is to have beta-iota reduction only at the positions where *) (* parameters are substituted *) - let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in + let typs = List.map (map_type (nf_betaiota !!(pb.env) !(pb.evdref))) typs in (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) @@ -1291,11 +1296,11 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs' = List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in - let extenv = push_rel_context typs pb.env in + let typs,extenv = push_rel_context !(pb.evdref) typs pb.env in let typs' = List.map (fun (c,d) -> - (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in + (c,extract_inductive_data !!extenv !(pb.evdref) d,d)) typs' in (* We compute over which of x(i+1)..xn and x matching on xi will need a *) (* generalization *) @@ -1360,7 +1365,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let submat = adjust_impossible_cases pb pred tomatch submat in let () = match submat with | [] -> - raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history)) + raise_pattern_matching_error (!!(pb.env), Evd.empty, NonExhaustive (complete_history history)) | _ -> () in @@ -1370,7 +1375,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn tomatch = tomatch; pred = pred; history = history; - mat = List.map (push_rels_eqn_with_names typs) submat } + mat = List.map (push_rels_eqn_with_names !(pb.evdref) typs) submat } (********************************************************************** INVARIANT: @@ -1400,13 +1405,13 @@ and match_current pb (initial,tomatch) = let ((current,typ),deps,dep) = tomatch in match typ with | NotInd (_,typ) -> - check_all_variables pb.env !(pb.evdref) typ pb.mat; + check_all_variables !!(pb.env) !(pb.evdref) typ pb.mat; compile_all_variables initial tomatch pb | IsInd (_,(IndType(indf,realargs) as indt),names) -> let mind,_ = dest_ind_family indf in - let mind = Tacred.check_privacy pb.env mind in - let cstrs = get_constructors pb.env indf in - let arsign, _ = get_arity pb.env indf in + let mind = Tacred.check_privacy !!(pb.env) mind in + let cstrs = get_constructors !!(pb.env) indf in + let arsign, _ = get_arity !!(pb.env) indf in let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in let no_cstr = Int.equal (Array.length cstrs) 0 in if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then @@ -1423,18 +1428,17 @@ and match_current pb (initial,tomatch) = postprocess_dependencies !(pb.evdref) depstocheck brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> - let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in it_mkLambda_or_LetIn body sign) brvals in let (pred,typ) = - find_predicate pb.caseloc pb.env pb.evdref + find_predicate pb.caseloc pb.env pb.evdref pred current indt (names,dep) tomatch in - let ci = make_case_info pb.env (fst mind) pb.casestyle in - let pred = nf_betaiota pb.env !(pb.evdref) pred in + let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in + let pred = nf_betaiota !!(pb.env) !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project !!(pb.env) !(pb.evdref) indf ci pred current brvals in - let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in - Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; + let _ = Evarutil.evd_comb1 (Typing.type_of !!(pb.env)) pb.evdref pred in + Typing.check_allowed_sort !!(pb.env) !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist !(pb.evdref) typ inst } @@ -1444,14 +1448,15 @@ and match_current pb (initial,tomatch) = and shift_problem ((current,t),_,na) pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in - let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in + let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in let pb = { pb with - env = push_rel (LocalDef (na,current,ty)) pb.env; + env = snd (push_rel !(pb.evdref) (LocalDef (na,current,ty)) env); tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; - mat = List.map (push_current_pattern (current,ty)) pb.mat } in + mat = List.map (push_current_pattern !(pb.evdref) (current,ty)) pb.mat } in let j = compile pb in { uj_val = subst1 current j.uj_val; uj_type = subst1 current j.uj_type } @@ -1461,7 +1466,7 @@ and shift_problem ((current,t),_,na) pb = are already introduced in the context, we avoid creating aliases to themselves by treating this case specially. *) and pop_problem ((current,t),_,na) pb = - let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in let pb = { pb with pred = pred; @@ -1483,9 +1488,9 @@ and compile_branch initial current realargs names deps pb arsign eqns cstr = and compile_generalization pb i d rest = let pb = { pb with - env = push_rel d pb.env; + env = snd (push_rel !(pb.evdref) d pb.env); tomatch = rest; - mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in + mat = List.map (push_generalized_decl_eqn pb.env !(pb.evdref) i d) pb.mat } in let j = compile pb in { uj_val = mkLambda_or_LetIn d j.uj_val; uj_type = mkProd_wo_LetIn d j.uj_type } @@ -1498,11 +1503,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = let alias = LocalDef (na,c,t) in let pb = { pb with - env = push_rel alias pb.env; + env = snd (push_rel !(pb.evdref) alias pb.env); tomatch = lift_tomatch_stack 1 rest; pred = lift_predicate 1 pb.pred pb.tomatch; history = pop_history_pattern pb.history; - mat = List.map (push_alias_eqn alias) pb.mat } in + mat = List.map (push_alias_eqn !(pb.evdref) alias) pb.mat } in let j = compile pb in let sigma = !(pb.evdref) in { uj_val = @@ -1534,7 +1539,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then (* Try to compile first using non expanded alias *) try - if initial then f orig (Retyping.get_type_of pb.env sigma orig) + if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig) else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) @@ -1549,7 +1554,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = (* Could be needed in case of a recursive call which requires to be on a variable for size reasons *) pb.evdref := sigma; - if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) + if initial then f orig (Retyping.get_type_of !!(pb.env) !(pb.evdref) orig) else just_pop () @@ -1573,7 +1578,7 @@ substituer après par les initiaux *) * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} = - let avoid = ids_of_named_context_val (named_context_val env) in + let avoid = ids_of_named_context_val (named_context_val !!env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = { rhs_env = env; @@ -1616,8 +1621,8 @@ let matx_of_eqns env eqns = *) let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = - let n = Context.Rel.length (rel_context env) in - let n' = Context.Rel.length (rel_context extenv) in + let n = Context.Rel.length (rel_context !!env) in + let n' = Context.Rel.length (rel_context !!extenv) in (* We first remove the bindings that are dependently typed (they are difficult to manage and it is not sure these are so useful in practice); Notes: @@ -1630,22 +1635,22 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *) (* \--env-/ (= x:ty) *) (* \--------------extenv------------/ *) - let (p, _, _) = lookup_rel_id x (rel_context extenv) in + let (p, _, _) = lookup_rel_id x (rel_context !!extenv) in let rec traverse_local_defs p = - match lookup_rel p extenv with + match lookup_rel p !!extenv with | LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c) | LocalAssum _ -> p in let p = traverse_local_defs p in let u = lift (n' - n) u in - try Some (p, u, expand_vars_in_term extenv sigma u) + try Some (p, u, expand_vars_in_term !!extenv sigma u) (* pedrot: does this really happen to raise [Failure _]? *) with Failure _ -> None in let subst0 = List.map_filter map subst in let t0 = lift (n' - n) t in (subst0, t0) -let push_binder d (k,env,subst) = - (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst) +let push_binder sigma d (k,env,subst) = + (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst) let rec list_assoc_in_triple x = function [] -> raise Not_found @@ -1667,7 +1672,7 @@ let rec list_assoc_in_triple x = function *) let abstract_tycon ?loc env evdref subst tycon extenv t = - let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) + let t = nf_betaiota !!env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk)) | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in @@ -1679,31 +1684,31 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = convertible subterms of the substitution *) let rec aux (k,env,subst as x) t = match EConstr.kind !evdref t with - | Rel n when is_local_def (lookup_rel n env) -> t + | Rel n when is_local_def (lookup_rel n !!env) -> t | Evar ev -> - let ty = get_type_of env !evdref t in - let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in + let ty = get_type_of !!env !evdref t in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty in let inst = List.map_i (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) - 1 (rel_context env) in - let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in - begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with + 1 (rel_context !!env) in + let ev' = evd_comb1 (Evarutil.new_evar !!env ~src) evdref ty in + begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false end; ev' | _ -> - let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in + let good = List.filter (fun (_,u,_) -> is_conv_leq !!env !evdref t u) subst in match good with | [] -> - map_constr_with_full_binders !evdref push_binder aux x t + map_constr_with_full_binders !evdref (push_binder !evdref) aux x t | (_, _, u) :: _ -> (* u is in extenv *) let vl = List.map pi1 good in let ty = - let ty = get_type_of env !evdref t in - Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty + let ty = get_type_of !!env !evdref t in + Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty in let dummy_subst = List.init k (fun _ -> mkProp) in let ty = substl dummy_subst (aux x ty) in @@ -1711,7 +1716,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = let inst = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 - (rel_context extenv) in + (rel_context !!extenv) in let map a = match EConstr.kind !evdref a with | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl | _ -> true @@ -1719,10 +1724,10 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = let rel_filter = List.map map inst in let named_filter = List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) - (named_context extenv) in + (named_context !!extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in + let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1732,19 +1737,19 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = | None -> (* This is the situation we are building a return predicate and we are in an impossible branch *) - let n = Context.Rel.length (rel_context env) in - let n' = Context.Rel.length (rel_context tycon_env) in + let n = Context.Rel.length (rel_context !!env) in + let n' = Context.Rel.length (rel_context !!tycon_env) in let impossible_case_type, u = evd_comb1 - (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) + (new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase)) evdref univ_flexible_alg in (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in - let tt = evd_comb1 (Typing.type_of extenv) evdref t in + let tt = evd_comb1 (Typing.type_of !!extenv) evdref t in (t,tt) in - match cumul env !evdref tt (mkSort s) with + match cumul !!env !evdref tt (mkSort s) with | None -> anomaly (Pp.str "Build_tycon: should be a type."); | Some sigma -> evdref := sigma; { uj_val = t; uj_type = tt } @@ -1761,14 +1766,14 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = - let id = next_name_away (named_hd env sigma t Anonymous) avoid in + let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in let rec reveal_pattern t (subst,avoid as acc) = - match EConstr.kind sigma (whd_all env sigma t) with + match EConstr.kind sigma (whd_all !!env sigma t) with | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in - let n = constructor_nrealargs_env env cstr in + let n = constructor_nrealargs_env !!env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_right_map reveal_pattern l acc in DAst.make (PatCstr (cstr,l,Anonymous)), acc @@ -1780,19 +1785,19 @@ let build_inversion_problem loc env sigma tms t = let patl,acc = List.fold_right_map reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env sigma true indf' in + let sign = make_arity_signature !!env sigma true indf' in let patl = pat :: List.rev patl in - let patl,sign = recover_and_adjust_alias_names patl sign in + let patl,sign = recover_and_adjust_alias_names acc patl sign in let p = List.length patl in - let env' = push_rel_context sign env in + let _,env' = push_rel_context sigma sign env in let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in let d = LocalAssum (alias_of_pat pat,typ) in - let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in + let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in - let avoid0 = vars_of_env env in + let avoid0 = GlobEnv.vars_of_env env in (* [patl] is a list of patterns revealing the substructure of constructors present in the constraints on the type of the multiple terms t1..tn that are matched in the original problem; @@ -1808,9 +1813,9 @@ let build_inversion_problem loc env sigma tms t = let decls = List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in - let pb_env = push_rel_context sign env in + let _,pb_env = push_rel_context sigma sign env in let decls = - List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in + List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in let decls = List.rev decls in let dep_sign = find_dependencies_signature sigma (List.make n true) decls in @@ -1843,7 +1848,7 @@ let build_inversion_problem loc env sigma tms t = constraints are incompatible with the constraints on the inductive types of the multiple terms matched in Xi *) let catch_all_eqn = - if List.for_all (irrefutable env) patl then + if List.for_all (irrefutable !!env) patl then (* No need for a catch all clause *) [] else @@ -1857,13 +1862,12 @@ let build_inversion_problem loc env sigma tms t = it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) - let s' = Retyping.get_sort_of env sigma t in + let s' = Retyping.get_sort_of !!env sigma t in let sigma, s = Evd.new_sort_variable univ_flexible sigma in - let sigma = Evd.set_leq_sort env sigma s' s in + let sigma = Evd.set_leq_sort !!env sigma s' s in let evdref = ref sigma in let pb = { env = pb_env; - lvar = empty_lvar; evdref = evdref; pred = (*ty *) mkSort s; tomatch = sub_tms; @@ -1878,16 +1882,16 @@ let build_inversion_problem loc env sigma tms t = (* Here, [pred] is assumed to be in the context built from all *) (* realargs and terms to match *) let build_initial_predicate arsign pred = - let rec buildrec n pred tmnames = function + let rec buildrec pred tmnames = function | [] -> List.rev tmnames,pred | (decl::realdecls)::lnames -> let na = RelDecl.get_name decl in - let n' = n + List.length realdecls in - buildrec (n'+1) pred (force_name na::tmnames) lnames + let realnames = List.map RelDecl.get_name realdecls in + buildrec pred ((force_name na,realnames)::tmnames) lnames | _ -> assert false - in buildrec 0 pred [] (List.rev arsign) + in buildrec pred [] (List.rev arsign) -let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = +let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let lift = if dolift then lift else fun n t -> t in let get_one_sign n tm (na,t) = match tm with @@ -1895,7 +1899,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = (match t with | None -> let sign = match bo with | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign + | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign | Some {CAst.loc} -> user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1905,31 +1909,23 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in let arsign = fst (get_arity env0 indf') in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in - let realnal, realnal' = + let realnal = match t with | Some {CAst.loc;v=(ind',realnal)} -> if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then anomaly (Pp.str "Ill-formed 'in' clause in cases."); - let realnal = List.rev realnal in - let realnal' = List.map (ltac_interp_name lvar) realnal in - realnal,realnal' + List.rev realnal | None -> - let realnal = List.make nrealargs_ctxt Anonymous in - realnal, realnal in - let na' = ltac_interp_name lvar na in + List.make nrealargs_ctxt Anonymous in let t = EConstr.of_constr (build_dependent_inductive env0 indf') in - (* Context with names for typing *) - let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in - (* Context with names for building the term *) - let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in - arsign1,arsign2 in + LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> let l = get_one_sign n tm x in - l :: buildrec (n + List.length (fst l)) (ltm,tmsign) + l :: buildrec (n + List.length l) (ltm,tmsign) | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) @@ -1986,9 +1982,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = in assert (len == 0); let p = predicate 0 c in - let env' = List.fold_right push_rel_context arsign env in - try let sigma' = fst (Typing.type_of env' sigma p) in - Some (sigma', p) + let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in + try let sigma' = fst (Typing.type_of !!env' sigma p) in + Some (sigma', p, arsign) with e when precatchable_exception e -> None (* Builds the predicate. If the predicate is dependent, its context is @@ -2017,15 +2013,14 @@ let noccur_with_meta sigma n m term = in try (occur_rec n term; true) with LocalOccur -> false -let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred = +let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = (** If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe can appear in the term. *) refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) - env sigma t + !!env sigma t in - let typing_arsign,building_arsign = List.split arsign in let preds = match pred, tycon with (* No return clause *) @@ -2035,12 +2030,12 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred (* First strategy: we abstract the tycon wrt to the dependencies *) let sigma, t = refresh_tycon sigma t in let p1 = - prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in + prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in (match p1 with - | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2] - | None -> [sigma2, pred2]) + | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign] + | None -> [sigma2, pred2, arsign]) | None, _ -> (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) @@ -2048,28 +2043,28 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred | Some t -> refresh_tycon sigma t | None -> let (sigma, (t, _)) = - new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in + new_type_evar !!env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in sigma, t in (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length (List.flatten typing_arsign)) t in - [sigma1, pred1; sigma, pred2] + let pred2 = lift (List.length (List.flatten arsign)) t in + [sigma1, pred1, arsign; sigma, pred2, arsign] (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let envar = List.fold_right push_rel_context typing_arsign env in + let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in let sigma, newt = new_sort_variable univ_flexible_alg sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in let sigma = !evdref in let predccl = nf_evar sigma predcclj.uj_val in - [sigma, predccl] + [sigma, predccl, building_arsign] in List.map - (fun (sigma,pred) -> - let (nal,pred) = build_initial_predicate building_arsign pred in + (fun (sigma,pred,arsign) -> + let (nal,pred) = build_initial_predicate arsign pred in sigma,nal,pred) preds @@ -2152,7 +2147,7 @@ let constr_of_pat env evdref arsign pat avoid = typ env (substl args liftt, []) ua avoid in let args' = arg' :: List.map (lift n') args in - let env' = push_rel_context sign' env in + let env' = EConstr.push_rel_context sign' env in (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) in @@ -2172,8 +2167,8 @@ let constr_of_pat env evdref arsign pat avoid = let avoid = Id.Set.add id avoid in let sign, i, avoid = try - let env = push_rel_context sign env in - evdref := the_conv_x_leq (push_rel_context sign env) + let env = EConstr.push_rel_context sign env in + evdref := the_conv_x_leq (EConstr.push_rel_context sign env) (lift (succ m) ty) (lift 1 apptype) !evdref; let eq_t = mk_eq evdref (lift (succ m) ty) (mkRel 1) (* alias *) @@ -2240,7 +2235,6 @@ let lift_rel_context n l = full signature. However prevpatterns are in the original one signature per pattern form. *) let build_ineqs evdref prevpatterns pats liftsign = - let _tomatchs = List.length pats in let diffs = List.fold_left (fun c eqnpats -> @@ -2288,7 +2282,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let _, newpatterns, pats = List.fold_left2 (fun (idents, newpatterns, pats) pat arsign -> - let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in + let pat', cpat, idents = constr_of_pat !!env evdref arsign pat idents in (idents, pat' :: newpatterns, cpat :: pats)) (Id.Set.empty, [], []) eqn.patterns sign in @@ -2315,7 +2309,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = in let ineqs = build_ineqs evdref prevpatterns pats signlen in let rhs_rels' = rels_of_patsign !evdref rhs_rels in - let _signenv = push_rel_context rhs_rels' env in + let _signenv,_ = push_rel_context !evdref rhs_rels' env in let arity = let args, nargs = List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> @@ -2335,11 +2329,11 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity in - let rhs_env = push_rel_context rhs_rels' env in + let _,rhs_env = push_rel_context !evdref rhs_rels' env in let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of !!env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = @@ -2492,10 +2486,10 @@ let context_of_arsign l = l ([], 0) in x -let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar +let compile_program_cases ?loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) = let typing_fun tycon env = function - | Some t -> typing_function tycon env evdref lvar t + | Some t -> typing_function tycon env evdref t | None -> Evarutil.evd_comb0 use_unit_judge evdref in (* We build the matrix of patterns and right-hand side *) @@ -2503,29 +2497,28 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in + let env,tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in let tycon = valcon_of_tycon tycon in let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in - let env = push_rel_context tomatchs_lets env in + let _,env = push_rel_context !evdref tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = (* The arity signature *) - let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in - let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *) + let arsign = extract_arity_signature ~dolift:false !!env tomatchs tomatchl in (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) let avoid = Id.Set.empty in - build_dependent_signature env evdref avoid tomatchs arsign + build_dependent_signature !!env evdref avoid tomatchs arsign in let tycon, arity = let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in match tycon' with - | None -> let ev = mkExistential env evdref in ev, lift nar ev + | None -> let ev = mkExistential !!env evdref in ev, lift nar ev | Some t -> let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with - | Some (evd, pred) -> evdref := evd; pred + | Some (evd, pred, arsign) -> evdref := evd; pred | None -> lift nar t in Option.get tycon, pred @@ -2541,7 +2534,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar in let matx = List.rev matx in let _ = assert (Int.equal len (List.length lets)) in - let env = push_rel_context lets env in + let _,env = push_rel_context !evdref lets env in let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in let args = List.rev_map (lift len) args in @@ -2554,10 +2547,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) | NotInd (Some b, t) -> LocalDef (na,b,t) | IsInd (typ,_,_) -> LocalAssum (na,typ) in - let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in + let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in let typs = - List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in + List.map (fun (c,d) -> (c,extract_inductive_data !!env !evdref d,d)) typs in let dep_sign = find_dependencies_signature !evdref @@ -2566,20 +2559,20 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let typs' = List.map3 - (fun (tm,tmt) deps na -> + (fun (tm,tmt) deps (na,realnames) -> let deps = if not (isRel !evdref tm) then [] else deps in + let tmt = set_tomatch_realnames realnames tmt in ((tm,tmt),deps,na)) tomatchs dep_sign nal in let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in let typing_function tycon env evdref = function - | Some t -> typing_function tycon env evdref lvar t + | Some t -> typing_function tycon env evdref t | None -> evd_comb0 use_unit_judge evdref in let pb = { env = env; - lvar = lvar; evdref = evdref; pred = pred; tomatch = initial_pushed; @@ -2591,7 +2584,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let j = compile pb in (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; + List.iter (check_unused_pattern !!env) matx; let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; @@ -2602,10 +2595,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) = +let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then compile_program_cases ?loc style (typing_fun, evdref) - tycon env lvar (predopt, tomatchl, eqns) + tycon env (predopt, tomatchl, eqns) else (* We build the matrix of patterns and right-hand side *) @@ -2613,15 +2606,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in - - + let predenv,tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in (* If an elimination predicate is provided, we check it is compatible with the type of arguments to match; if none is provided, we build alternative possible predicates *) - let arsign = extract_arity_signature env predlvar tomatchs tomatchl in - let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in + let arsign = extract_arity_signature !!env tomatchs tomatchl in + let preds = prepare_predicate ?loc typing_fun predenv !evdref tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) @@ -2631,10 +2622,10 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) | NotInd (Some b,t) -> LocalDef (na,b,t) | IsInd (typ,_,_) -> LocalAssum (na,typ) in - let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in + let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in let typs = - List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in + List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in let dep_sign = find_dependencies_signature !evdref @@ -2643,8 +2634,9 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat let typs' = List.map3 - (fun (tm,tmt) deps na -> + (fun (tm,tmt) deps (na,realnames) -> let deps = if not (isRel !evdref tm) then [] else deps in + let tmt = set_tomatch_realnames realnames tmt in ((tm,tmt),deps,na)) tomatchs dep_sign nal in @@ -2652,14 +2644,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat (* A typing function that provides with a canonical term for absurd cases*) let typing_fun tycon env evdref = function - | Some t -> typing_fun tycon env evdref lvar t + | Some t -> typing_fun tycon env evdref t | None -> evd_comb0 use_unit_judge evdref in let myevdref = ref sigma in let pb = { env = env; - lvar = lvar; evdref = myevdref; pred = pred; tomatch = initial_pushed; @@ -2672,7 +2663,7 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat let j = compile pb in (* We coerce to the tycon (if an elim predicate was provided) *) - let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in + let j = inh_conv_coerce_to_tycon ?loc !!env myevdref j tycon in evdref := !myevdref; j in @@ -2681,6 +2672,6 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat let j = list_try_compile compile_for_one_predicate preds in (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; + List.iter (check_unused_pattern !!env) matx; j diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 04a3464679..76b81a58c1 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -15,7 +15,6 @@ open Environ open EConstr open Inductiveops open Glob_term -open Ltac_pretype open Evardefine (** {5 Compilation of pattern-matching } *) @@ -42,9 +41,9 @@ val irrefutable : env -> cases_pattern -> bool val compile_cases : ?loc:Loc.t -> case_style -> - (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref -> + (type_constraint -> GlobEnv.t -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses -> + GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment val constr_of_pat : @@ -59,7 +58,7 @@ val constr_of_pat : Names.Id.Set.t type 'a rhs = - { rhs_env : env; + { rhs_env : GlobEnv.t; rhs_vars : Id.Set.t; avoid_ids : Id.Set.t; it : 'a option} @@ -103,8 +102,7 @@ and pattern_continuation = | Result of cases_pattern list type 'a pattern_matching_problem = - { env : env; - lvar : Ltac_pretype.ltac_var_map; + { env : GlobEnv.t; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -112,21 +110,19 @@ type 'a pattern_matching_problem = mat : 'a matrix; caseloc : Loc.t option; casestyle : case_style; - typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } - + typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment } val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : ?loc:Loc.t -> (type_constraint -> - Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> - Environ.env -> + GlobEnv.t -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) -> + GlobEnv.t -> Evd.evar_map -> - Ltac_pretype.ltac_var_map -> (types * tomatch_type) list -> - (rel_context * rel_context) list -> + rel_context list -> constr option -> - glob_constr option -> (Evd.evar_map * Name.t list * constr) list + glob_constr option -> (Evd.evar_map * (Name.t * Name.t list) list * constr) list -val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t -> - Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map +val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Name.t -> + Glob_term.glob_constr -> constr -> GlobEnv.t diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 542fb5456c..332ecd2c91 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -16,7 +16,6 @@ open Constr open Libnames open Globnames open Nametab -open Environ open Libobject open Mod_subst @@ -118,6 +117,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -131,12 +133,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -316,16 +319,16 @@ let lookup_pattern_path_between env (s,t) = (* rajouter une coercion dans le graphe *) -let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = - ref (fun _ _ _ -> str "<a class path>") +let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path env sigma x = !path_printer env sigma x +let print_path x = !path_printer x -let message_ambig env sigma l = +let message_ambig l = str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l + prlist_with_sep fnl print_path l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -339,7 +342,7 @@ let different_class_params i = | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false -let add_coercion_in_graph env sigma (ic,source,target) = +let add_coercion_in_graph (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -381,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig env sigma !ambig_paths) + Feedback.msg_info (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -426,7 +429,7 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion env sigma (_, c) = +let cache_coercion (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in @@ -439,15 +442,22 @@ let cache_coercion env sigma (_, c) = coe_param = c.coercion_params; } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph env sigma (xf,is,it) + add_coercion_in_graph (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + cache_coercion o + +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -492,8 +502,8 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn - ); + set_coercion_in_scope objn; + cache_coercion objn); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } @@ -553,3 +563,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..7c4842c8ae 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -99,7 +99,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) @@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option + +val is_coercion_in_scope : GlobRef.t -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5e3821edf1..e15c00f7dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -363,12 +363,20 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +let warn_coercion_not_in_scope = + CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated" + Pp.(fun r -> str "Coercion used but not in scope: " ++ + Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use " + ++ str "this coercion, please Import the module that contains it.") + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> + if not (is_coercion_in_scope i.coe_value) then + warn_coercion_not_in_scope i.coe_value; let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in @@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml new file mode 100644 index 0000000000..12788e5ec5 --- /dev/null +++ b/pretyping/globEnv.ml @@ -0,0 +1,201 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Pp +open CErrors +open Names +open Environ +open EConstr +open Evarutil +open Termops +open Vars +open Ltac_pretype + +(** This files provides a level of abstraction for the kind of + environment used for type inference (so-called pretyping); in + particular: + - it supports that term variables can be interpreted as Ltac + variables pointing to the effective expected name + - it incrementally and lazily computes the renaming of rel + variables used to build purely-named evar contexts +*) + +type t = { + static_env : env; + (** For locating indices *) + renamed_env : env; + (** For name management *) + extra : ext_named_context Lazy.t; + (** Delay the computation of the evar extended environment *) + lvar : ltac_var_map; +} + +let make env sigma lvar = + let get_extra env sigma = + let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) in + { + static_env = env; + renamed_env = env; + extra = lazy (get_extra env sigma); + lvar = lvar; + } + +let env env = env.static_env + +let vars_of_env env = + Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env) + +let ltac_interp_name { ltac_idents ; ltac_genargs } = function + | Anonymous -> Anonymous + | Name id as na -> + try Name (Id.Map.find id ltac_idents) + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ + spc () ++ str "is not bound to an identifier." ++ + spc () ++str "It cannot be used in a binder.") + else na + +let push_rel sigma d env = + let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in + let env = { + static_env = push_rel d env.static_env; + renamed_env = push_rel d' env.renamed_env; + extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra)); + lvar = env.lvar; + } in + d', env + +let push_rel_context ?(force_names=false) sigma ctx env = + let open Context.Rel.Declaration in + let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in + let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in + let env = { + static_env = push_rel_context ctx env.static_env; + renamed_env = push_rel_context ctx' env.renamed_env; + extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra)); + lvar = env.lvar; + } in + ctx', env + +let push_rec_types sigma (lna,typarray) env = + let open Context.Rel.Declaration in + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in + Array.map get_name ctx, env + +let e_new_evar env evdref ?src ?naming typ = + let open Context.Named.Declaration in + let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in + let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in + let (subst, _, nc) = Lazy.force env.extra in + let typ' = csubst_subst subst typ in + let instance = inst_rels @ inst_vars in + let sign = val_of_named_context nc in + let sigma = !evdref in + let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := sigma; + e + +let e_new_type_evar env evdref ~src = + let (evd', s) = Evd.new_sort_variable Evd.univ_flexible_alg !evdref in + evdref := evd'; + e_new_evar env evdref ~src (EConstr.mkSort s) + +let hide_variable env expansion id = + let lvar = env.lvar in + if Id.Map.mem id lvar.ltac_genargs then + let lvar = match expansion with + | Name id' -> + (* We are typically in a situation [match id return P with ... end] + which we interpret as [match id' as id' return P with ... end], + with [P] interpreted in an environment where [id] is bound to [id']. + The variable is already bound to [id'], so nothing to do *) + lvar + | _ -> + (* We are typically in a situation [match id return P with ... end] + with [id] bound to a non-variable term [c]. We interpret as + [match c as id return P with ... end], and hides [id] while + interpreting [P], since it has become a binder and cannot be anymore be + substituted by a variable coming from the Ltac substitution. *) + { lvar with + ltac_uconstrs = Id.Map.remove id lvar.ltac_uconstrs; + ltac_constrs = Id.Map.remove id lvar.ltac_constrs; + ltac_genargs = Id.Map.remove id lvar.ltac_genargs } in + { env with lvar } + else + env + +let protected_get_type_of env sigma c = + try Retyping.get_type_of ~lax:true env sigma c + with Retyping.RetypeError _ -> + user_err + (str "Cannot reinterpret " ++ quote (print_constr c) ++ + str " in the current environment.") + +let invert_ltac_bound_name env id0 id = + try mkRel (pi1 (lookup_rel_id id (rel_context env.static_env))) + with Not_found -> + user_err (str "Ltac variable " ++ Id.print id0 ++ + str " depends on pattern variable name " ++ Id.print id ++ + str " which is not bound in current context.") + +let interp_ltac_variable ?loc typing_fun env sigma id = + (* Check if [id] is an ltac variable *) + try + let (ids,c) = Id.Map.find id env.lvar.ltac_constrs in + let subst = List.map (invert_ltac_bound_name env id) ids in + let c = substl subst c in + { uj_val = c; uj_type = protected_get_type_of env.renamed_env sigma c } + with Not_found -> + try + let {closure;term} = Id.Map.find id env.lvar.ltac_uconstrs in + let lvar = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; } + in + (* spiwack: I'm catching [Not_found] potentially too eagerly + here, as the call to the main pretyping function is caught + inside the try but I want to avoid refactoring this function + too much for now. *) + typing_fun {env with lvar} term + with Not_found -> + (* Check if [id] is a ltac variable not bound to a term *) + (* and build a nice error message *) + if Id.Map.mem id env.lvar.ltac_genargs then begin + let Geninterp.Val.Dyn (typ, _) = Id.Map.find id env.lvar.ltac_genargs in + user_err ?loc + (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ + bound to a " ++ Geninterp.Val.pr typ ++ str ".") + end; + raise Not_found + +module ConstrInterpObj = +struct + type ('r, 'g, 't) obj = + unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map + let name = "constr_interp" + let default _ = None +end + +module ConstrInterp = Genarg.Register(ConstrInterpObj) + +let register_constr_interp0 = ConstrInterp.register0 + +let interp_glob_genarg env sigma ty arg = + let open Genarg in + let GenArg (Glbwit tag, arg) = arg in + let interp = ConstrInterp.obj tag in + interp env.lvar.ltac_genargs env.renamed_env sigma ty arg diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli new file mode 100644 index 0000000000..4038523211 --- /dev/null +++ b/pretyping/globEnv.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Environ +open Evd +open EConstr +open Ltac_pretype + +(** To embed constr in glob_constr *) + +val register_constr_interp0 : + ('r, 'g, 't) Genarg.genarg_type -> + (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit + +(** {6 Pretyping name management} *) + +(** The following provides a level of abstraction for the kind of + environment used for type inference (so-called pretyping); in + particular: + - it supports that term variables can be interpreted as Ltac + variables pointing to the effective expected name + - it incrementally and lazily computes the renaming of rel + variables used to build purely-named evar contexts +*) + +(** Type of environment extended with naming and ltac interpretation data *) + +type t + +(** Build a pretyping environment from an ltac environment *) + +val make : env -> evar_map -> ltac_var_map -> t + +(** Export the underlying environement *) + +val env : t -> env + +val vars_of_env : t -> Id.Set.t + +(** Push to the environment, returning the declaration(s) with interpreted names *) + +val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t +val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t +val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t + +(** Declare an evar using renaming information *) + +val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> + ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr + +val e_new_type_evar : t -> evar_map ref -> src:Evar_kinds.t Loc.located -> constr + +(** [hide_variable env na id] tells to hide the binding of [id] in + the ltac environment part of [env] and to additionally rebind + it to [id'] in case [na] is some [Name id']. It is useful e.g. + for the dual status of [y] as term and binder. This is the case + of [match y return p with ... end] which implicitly denotes + [match z as z return p with ... end] when [y] is bound to a + variable [z] and [match t as y return p with ... end] when [y] + is bound to a non-variable term [t]. In the latter case, the + binding of [y] to [t] should be hidden in [p]. *) + +val hide_variable : t -> Name.t -> Id.t -> t + +(** In case a variable is not bound by a term binder, look if it has + an interpretation as a term in the ltac_var_map *) + +val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) -> + t -> evar_map -> Id.t -> unsafe_judgment + +(** Interpreting a generic argument, typically a "ltac:(...)", taking + into account the possible renaming *) + +val interp_glob_genarg : t -> evar_map -> constr -> + Genarg.glob_generic_argument -> constr * evar_map diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 24eb666828..bd13f1d00a 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -15,7 +15,6 @@ open Nameops open Globnames open Glob_term open Evar_kinds -open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) @@ -577,22 +576,9 @@ let glob_constr_of_closed_cases_pattern p = match DAst.get p with let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p -(**********************************************************************) -(* Interpreting ltac variables *) - -open Pp -open CErrors - -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as n -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - user_err (str"Ltac variable"++spc()++ Id.print id ++ - spc()++str"is not bound to an identifier."++spc()++ - str"It cannot be used in a binder.") - else n +(* This has to be in some file... *) + +open Ltac_pretype let empty_lvar : ltac_var_map = { ltac_constrs = Id.Map.empty; diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c967f4e884..91a2ef9c1e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -101,5 +101,4 @@ val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index eb283a0220..be79b8b07d 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FEvar ((_,args),e) -> let variances = infer_stack infos variances stk in infer_vect infos variances (Array.map (mk_clos e) args) - | FRel _ -> variances + | FRel _ -> infer_stack infos variances stk | FFlex fl -> let variances = infer_table_key infos variances fl in infer_stack infos variances stk diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml index be8579c2e5..ac59b96eef 100644 --- a/pretyping/ltac_pretype.ml +++ b/pretyping/ltac_pretype.ml @@ -64,5 +64,5 @@ type ltac_var_map = { ltac_idents: Id.t Id.Map.t; (** Ltac variables bound to identifiers *) ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) + (** All Ltac variables (to pass on ltac subterms, and for error reporting) *) } diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a315376aca..d10c00fa6e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -38,19 +38,20 @@ open Reductionops open Type_errors open Typing open Globnames -open Nameops open Evarutil open Evardefine open Pretype_errors open Glob_term open Glob_ops +open GlobEnv open Evarconv -open Ltac_pretype module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +let (!!) env = GlobEnv.env env + (************************************************************************) (* This concerns Cases *) open Inductive @@ -58,58 +59,6 @@ open Inductiveops (************************************************************************) -module ExtraEnv = -struct - -type t = { - env : Environ.env; - extra : Evarutil.ext_named_context Lazy.t; - (** Delay the computation of the evar extended environment *) -} - -let get_extra env sigma = - let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) - (rel_context env) ~init:(empty_csubst, avoid, named_context env) - -let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } -let rel_context env = rel_context env.env - -let push_rel sigma d env = { - env = push_rel d env.env; - extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra)); -} - -let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma - -let push_rel_context sigma ctx env = { - env = push_rel_context ctx env.env; - extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra)); -} - -let lookup_named id env = lookup_named id env.env - -let e_new_evar env evdref ?src ?naming typ = - let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in - let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in - let (subst, _, nc) = Lazy.force env.extra in - let typ' = csubst_subst subst typ in - let instance = inst_rels @ inst_vars in - let sign = val_of_named_context nc in - let sigma = !evdref in - let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in - evdref := sigma; - e - -let push_rec_types sigma (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in - Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt - -end - -open ExtraEnv - (* An auxiliary function for searching for fixpoint guard indexes *) exception Found of int array @@ -400,7 +349,7 @@ let adjust_evar_source evdref na c = let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc !!env) evdref j t let check_instance loc subst = function | [] -> () @@ -417,76 +366,21 @@ let orelse_name name name' = match name with | Anonymous -> name' | _ -> name -let ltac_interp_name_env k0 lvar env sigma = - (* envhd is the initial part of the env when pretype was called first *) - (* (in practice is is probably 0, but we have to grant the - specification of pretype which accepts to start with a non empty - rel_context) *) - (* tail is the part of the env enriched by pretyping *) - let n = Context.Rel.length (rel_context env) - k0 in - let ctxt,_ = List.chop n (rel_context env) in - let open Context.Rel.Declaration in - let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in - if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env - else push_rel_context sigma ctxt' (pop_rel_context n env sigma) - -let invert_ltac_bound_name lvar env id0 id = - let id' = Id.Map.find id lvar.ltac_idents in - try mkRel (pi1 (lookup_rel_id id' (rel_context env))) - with Not_found -> - user_err (str "Ltac variable " ++ Id.print id0 ++ - str " depends on pattern variable name " ++ Id.print id ++ - str " which is not bound in current context.") - -let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c - with Retyping.RetypeError _ -> - user_err - (str "Cannot reinterpret " ++ quote (print_constr c) ++ - str " in the current environment.") - -let pretype_id pretype k0 loc env evdref lvar id = - let sigma = !evdref in +let pretype_id pretype k0 loc env evdref id = (* Look for the binder of [id] *) try - let (n,_,typ) = lookup_rel_id id (rel_context env) in + let (n,_,typ) = lookup_rel_id id (rel_context !!env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> - let env = ltac_interp_name_env k0 lvar env !evdref in - (* Check if [id] is an ltac variable *) - try - let (ids,c) = Id.Map.find id lvar.ltac_constrs in - let subst = List.map (invert_ltac_bound_name lvar env id) ids in - let c = substl subst c in - { uj_val = c; uj_type = protected_get_type_of env sigma c } - with Not_found -> try - let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in - let lvar = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; } - in - (* spiwack: I'm catching [Not_found] potentially too eagerly - here, as the call to the main pretyping function is caught - inside the try but I want to avoid refactoring this function - too much for now. *) - pretype env evdref lvar term - with Not_found -> - (* Check if [id] is a ltac variable not bound to a term *) - (* and build a nice error message *) - if Id.Map.mem id lvar.ltac_genargs then begin - let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in - user_err ?loc - (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ - bound to a " ++ Geninterp.Val.pr typ ++ str ".") - end; - (* Check if [id] is a section or goal variable *) - try - { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } - with Not_found -> - (* [id] not found, standard error message *) - error_var_not_found ?loc id + try + GlobEnv.interp_ltac_variable ?loc (fun env -> pretype env evdref) env !evdref id + with Not_found -> + (* Check if [id] is a section or goal variable *) + try + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) } + with Not_found -> + (* [id] not found, standard error message *) + error_var_not_found ?loc id (*************************************************************************) (* Main pretyping function *) @@ -524,18 +418,18 @@ let pretype_global ?loc rigid env evd gr us = match us with | None -> evd, None | Some l -> - let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in + let _, ctx = Global.constr_of_global_in_context !!env gr in let len = Univ.AUContext.size ctx in interp_instance ?loc evd ~len l in - let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr in (sigma, c) let pretype_ref ?loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -544,7 +438,7 @@ let pretype_ref ?loc evdref env ref us = | ref -> let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = unsafe_type_of env.ExtraEnv.env evd c in + let ty = unsafe_type_of !!env evd c in make_judge c ty let judge_of_Type ?loc evd s = @@ -560,31 +454,13 @@ let pretype_sort ?loc evdref = function | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s let new_type_evar env evdref loc = - let sigma = !evdref in - let (sigma, (e, _)) = - Evarutil.new_type_evar env.ExtraEnv.env sigma - univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) - in - evdref := sigma; - e - -module ConstrInterpObj = -struct - type ('r, 'g, 't) obj = - unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map - let name = "constr_interp" - let default _ = None -end - -module ConstrInterp = Genarg.Register(ConstrInterpObj) - -let register_constr_interp0 = ConstrInterp.register0 + e_new_type_evar env evdref ~src:(Loc.tag ?loc Evar_kinds.InternalHole) (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref t = let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in @@ -598,7 +474,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GVar id -> inh_conv_coerce_to_tycon ?loc env evdref - (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) + (pretype_id (fun e r t -> pretype tycon e r t) k0 loc env evdref id) tycon | GEvar (id, inst) -> @@ -609,13 +485,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre with Not_found -> user_err ?loc (str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in - let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in + let args = pretype_instance k0 resolve_tc env evdref loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in + let j = (Retyping.get_judgment_of !!env !evdref c) in inh_conv_coerce_to_tycon ?loc env evdref j tycon | GPatVar kind -> - let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -624,48 +499,40 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> - let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty - | None -> - new_type_evar env evdref loc in + | None -> new_type_evar env evdref loc in { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (k, _naming, Some arg) -> - let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty - | None -> - new_type_evar env evdref loc in - let open Genarg in - let ist = lvar.ltac_genargs in - let GenArg (Glbwit tag, arg) = arg in - let interp = ConstrInterp.obj tag in - let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in + | None -> new_type_evar env evdref loc in + let (c, sigma) = GlobEnv.interp_glob_genarg env !evdref ty arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } | GRec (fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function - [] -> ctxt + | [] -> ctxt | (na,bk,None,ty)::bl -> - let ty' = pretype_type empty_valcon env evdref lvar ty in + let ty' = pretype_type empty_valcon env evdref ty in let dcl = LocalAssum (na, ty'.utj_val) in - let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in - type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl + let dcl', env = push_rel !evdref dcl env in + type_bl env (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> - let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in + let ty' = pretype_type empty_valcon env evdref ty in + let bd' = pretype (mk_tycon ty'.utj_val) env evdref bd in let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in - let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in - type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in + let dcl', env = push_rel !evdref dcl env in + type_bl env (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> - pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar) + pretype_type empty_valcon (snd (push_rel_context !evdref e env)) evdref ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -678,14 +545,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GFix (vn,i) -> i | GCoFix i -> i in - begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with + begin match conv !!env !evdref ftys.(fixi) t with | None -> () | Some sigma -> evdref := sigma end | None -> () in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types !evdref (names,ftys,[||]) env in + let names,newenv = push_rec_types !evdref (names,ftys) env in let vdefj = Array.map2_i (fun i ctxt def -> @@ -694,12 +561,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (ctxt,ty) = decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in - let nenv = push_rel_context !evdref ctxt newenv in - let j = pretype (mk_tycon ty) nenv evdref lvar def in + let ctxt,nenv = push_rel_context !evdref ctxt newenv in + let j = pretype (mk_tycon ty) nenv evdref def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj; + evdref := Typing.check_type_fixpoint ?loc !!env !evdref names ftys vdefj; let nf c = nf_evar !evdref c in let ftys = Array.map nf ftys in (** FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in @@ -721,13 +588,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) + ?loc !!env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let fixdecls = (names,ftys,fdefs) in let cofix = (i, fixdecls) in - (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) + (try check_cofix !!env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in @@ -742,11 +609,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GProj (p, c) -> (* TODO: once GProj is used as an input syntax, use bidirectional typing here *) - let cj = pretype empty_tycon env evdref lvar c in - judge_of_projection env.ExtraEnv.env !evdref p cj + let cj = pretype empty_tycon env evdref c in + judge_of_projection !!env !evdref p cj | GApp (f,args) -> - let fj = pretype empty_tycon env evdref lvar f in + let fj = pretype empty_tycon env evdref f in let floc = loc_of_glob_constr f in let length = List.length args in let candargs = @@ -762,7 +629,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in + let IndType (indf, args) = find_rectype !!env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then List.map EConstr.of_constr pars else (* Let the usual code throw an error *) [] @@ -784,17 +651,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in - let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc !!env) evdref resj in + let resty = whd_all !!env !evdref resj.uj_type in match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> let tycon = Some c1 in - let hj = pretype tycon env evdref lvar c in + let hj = pretype tycon env evdref c in let candargs, ujval = match candargs with | [] -> [], j_val hj | arg :: args -> - begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with + begin match conv !!env !evdref (j_val hj) arg with | Some sigma -> evdref := sigma; args, nf_evar !evdref (j_val hj) | None -> @@ -807,104 +674,96 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre apply_rec env (n+1) j candargs rest | _ -> - let hj = pretype empty_tycon env evdref lvar c in + let hj = pretype empty_tycon env evdref c in error_cant_apply_not_functional - ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref + ?loc:(Loc.merge_opt floc argloc) !!env !evdref resj [|hj|] in let resj = apply_rec env 1 fj candargs args in let resj = match EConstr.kind !evdref resj.uj_val with | App (f,args) -> - if is_template_polymorphic env.ExtraEnv.env !evdref f then + if is_template_polymorphic !!env !evdref f then (* Special case for inductive type applications that must be refreshed right away. *) let c = mkApp (f, args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in - let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) !!env) evdref c in + let t = Retyping.get_type_of !!env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLambda(name,bk,c1,c2) -> + | GLambda(name,bk,c1,c2) -> let tycon' = evd_comb1 (fun evd tycon -> match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod ?loc !!env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon ?loc !!env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in - let j = pretype_type dom_valcon env evdref lvar c1 in - (* The name specified by ltac is used also to create bindings. So - the substitution must also be applied on variables before they are - looked up in the rel context. *) + let j = pretype_type dom_valcon env evdref c1 in let var = LocalAssum (name, j.utj_val) in - let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in - let name = ltac_interp_name lvar name in - let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in + let var',env' = push_rel !evdref var env in + let j' = pretype rng env' evdref c2 in + let name = get_name var' in + let resj = judge_of_abstraction !!env (orelse_name name name') j j' in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GProd(name,bk,c1,c2) -> - let j = pretype_type empty_valcon env evdref lvar c1 in - (* The name specified by ltac is used also to create bindings. So - the substitution must also be applied on variables before they are - looked up in the rel context. *) - let j' = match name with + | GProd(name,bk,c1,c2) -> + let j = pretype_type empty_valcon env evdref c1 in + let name, j' = match name with | Anonymous -> - let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = lift 1 j.utj_val } + let j = pretype_type empty_valcon env evdref c2 in + name, { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = LocalAssum (name, j.utj_val) in - let env' = push_rel !evdref var env in - pretype_type empty_valcon env' evdref lvar c2 + let var, env' = push_rel !evdref var env in + get_name var, pretype_type empty_valcon env' evdref c2 in - let name = ltac_interp_name lvar name in let resj = try - judge_of_product env.ExtraEnv.env name j j' + judge_of_product !!env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLetIn(name,c1,t,c2) -> + | GLetIn(name,c1,t,c2) -> let tycon1 = match t with | Some t -> - mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val + mk_tycon (pretype_type empty_valcon env evdref t).utj_val | None -> empty_tycon in - let j = pretype tycon1 env evdref lvar c1 in + let j = pretype tycon1 env evdref c1 in let t = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env) evdref j.uj_type in - (* The name specified by ltac is used also to create bindings. So - the substitution must also be applied on variables before they are - looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in - let name = ltac_interp_name lvar name in + let var, env = push_rel !evdref var env in + let j' = pretype tycon env evdref c2 in + let name = get_name var in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } | GLetTuple (nal,(na,po),c,d) -> - let cj = pretype empty_tycon env evdref lvar c in + let cj = pretype empty_tycon env evdref c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref cj.uj_type + try find_rectype !!env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj + error_case_not_inductive ?loc:cloc !!env !evdref cj in let ind = fst (fst (dest_ind_family indf)) in - let cstrs = get_constructors env.ExtraEnv.env indf in + let cstrs = get_constructors !!env indf in if not (Int.equal (Array.length cstrs) 1) then user_err ?loc (str "Destructing let is only for inductive types" ++ str " with one constructor."); @@ -914,7 +773,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre int cs.cs_nargs ++ str " variables."); let fsign, record = let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in - match Environ.get_projections env.ExtraEnv.env ind with + match Environ.get_projections !!env ind with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> @@ -933,108 +792,97 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fsign = if Flags.version_strictly_greater Flags.V8_6 then Context.Rel.map (whd_betaiota !evdref) fsign else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in + let fsign,env_f = push_rel_context !evdref fsign env in let obj ind p v f = - if not record then - let nal = List.map (fun na -> ltac_interp_name lvar na) nal in - let nal = List.rev nal in - let fsign = List.map2 set_name nal fsign in + if not record then let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in + let ci = make_case_info !!env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in - let env_f = push_rel_context !evdref fsign env in - (* Make dependencies from arity signature impossible *) + (* Make dependencies from arity signature impossible *) let arsgn = - let arsgn,_ = get_arity env.ExtraEnv.env indf in + let arsgn,_ = get_arity !!env indf in List.map (set_name Anonymous) arsgn in - let indt = build_dependent_inductive env.ExtraEnv.env indf in + let indt = build_dependent_inductive !!env indf in let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) - let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in - let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in - let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in - let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in + let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in let nar = List.length arsgn in + let psign',env_p = push_rel_context ~force_names:true !evdref psign predenv in (match po with | Some p -> - let env_p = push_rel_context !evdref psign env in - let pj = pretype_type empty_valcon env_p evdref predlvar p in + let pj = pretype_type empty_valcon env_p evdref p in let ccl = nf_evar !evdref pj.utj_val in let p = it_mkLambda_or_LetIn ccl psign' in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in - let fj = pretype (mk_tycon fty) env_f evdref lvar d in + let fty = hnf_lam_applist !!env !evdref lp inst in + let fj = pretype (mk_tycon fty) env_f evdref d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort !!env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let fj = pretype tycon env_f evdref predlvar d in + let fj = pretype tycon env_f evdref d in let ccl = nf_evar !evdref fj.uj_type in let ccl = if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type ?loc env.ExtraEnv.env !evdref + error_cant_find_case_type ?loc !!env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort !!env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) | GIf (c,(na,po),b1,b2) -> - let cj = pretype empty_tycon env evdref lvar c in + let cj = pretype empty_tycon env evdref c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref cj.uj_type + try find_rectype !!env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in - let cstrs = get_constructors env.ExtraEnv.env indf in + error_case_not_inductive ?loc:cloc !!env !evdref cj in + let cstrs = get_constructors !!env indf in if not (Int.equal (Array.length cstrs) 2) then user_err ?loc (str "If is only for inductive types with two constructors."); let arsgn = - let arsgn,_ = get_arity env.ExtraEnv.env indf in + let arsgn,_ = get_arity !!env indf in (* 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 + let indt = build_dependent_inductive !!env indf in let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) - let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in - let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in - let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in - let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in + let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in + let psign,env_p = push_rel_context !evdref psign predenv in let pred,p = match po with | Some p -> - let env_p = push_rel_context !evdref psign env in - let pj = pretype_type empty_valcon env_p evdref predlvar p in + let pj = pretype_type empty_valcon env_p evdref p in let ccl = nf_evar !evdref pj.utj_val in - let pred = it_mkLambda_or_LetIn ccl psign' in + let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in pred, typ | None -> let p = match tycon with | Some ty -> ty - | None -> - let env = ltac_interp_name_env k0 lvar env !evdref in - new_type_evar env evdref loc + | None -> new_type_evar env evdref loc in - it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in + it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = @@ -1049,85 +897,83 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let csgn = 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 + let _,env_c = push_rel_context !evdref csgn env in + let bj = pretype (mk_tycon pi) env_c evdref b in it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in + let ci = make_case_info !!env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort !!env !evdref ind cj.uj_val pred; mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in inh_conv_coerce_to_tycon ?loc env evdref cj tycon | GCases (sty,po,tml,eqns) -> - Cases.compile_cases ?loc sty - ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref) - tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns) + Cases.compile_cases ?loc sty (pretype,evdref) tycon env (po,tml,eqns) | GCast (c,k) -> let cj = match k with | CastCoerce -> - let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base ?loc env.ExtraEnv.env) evdref cj + let cj = pretype empty_tycon env evdref c in + evd_comb1 (Coercion.inh_coerce_to_base ?loc !!env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in - let tj = pretype_type empty_valcon env evdref lvar t in + let tj = pretype_type empty_valcon env evdref t in let tval = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env) evdref tj.utj_val in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> - let cj = pretype empty_tycon env evdref lvar c in + let cj = pretype empty_tycon env evdref c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + match Reductionops.vm_infer_conv !!env !evdref cty tval with | Some evd -> (evdref := evd; cj, tval) | None -> - error_actual_type ?loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + error_actual_type ?loc !!env !evdref cj tval + (ConversionFailed (!!env,cty,tval)) else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> - let cj = pretype empty_tycon env evdref lvar c in + let cj = pretype empty_tycon env evdref c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + match Nativenorm.native_infer_conv !!env !evdref cty tval with | Some evd -> (evdref := evd; cj, tval) | None -> - error_actual_type ?loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + error_actual_type ?loc !!env !evdref cj tval + (ConversionFailed (!!env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c, tval + pretype (mk_tycon tval) env evdref c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon ?loc env evdref cj tycon -and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = +and pretype_instance k0 resolve_tc env evdref loc hyps evk update = let f decl (subst,update) = let id = NamedDecl.get_id decl in let t = replace_vars subst (NamedDecl.get_type decl) in let c, update = try let c = List.assoc id update in - let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in + let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in c.uj_val, List.remove_assoc id update with Not_found -> try - let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found + let (n,_,t') = lookup_rel_id id (rel_context !!env) in + if is_conv !!env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try - let t' = env |> lookup_named id |> NamedDecl.get_type in - if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found + let t' = !!env |> lookup_named id |> NamedDecl.get_type in + if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1137,19 +983,19 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = check_instance loc subst inst; Array.map_of_list snd subst -(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with +(* [pretype_type valcon env evdref c] coerces [c] into a type *) +and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) evdref c = match DAst.get c with | GHole (knd, naming, None) -> let loc = loc_of_glob_constr c in (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with + let t = Retyping.get_type_of !!env sigma v in + match EConstr.kind sigma (whd_all !!env sigma t) with | Sort s -> ESorts.kind sigma s | Evar ev when is_Type sigma (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev + evd_comb1 (define_evar_as_sort !!env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in (* Correction of bug #5315 : we need to define an evar for *all* holes *) @@ -1160,40 +1006,39 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D { utj_val = v; utj_type = s } | None -> - let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | _ -> - let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in + let j = pretype k0 resolve_tc empty_tycon env evdref c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc !!env) evdref j in match valcon with | None -> tj | Some v -> - begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with + begin match cumul !!env !evdref v tj.utj_val with | Some sigma -> evdref := sigma; tj | None -> error_unexpected_type - ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + ?loc:(loc_of_glob_constr c) !!env !evdref tj.utj_val v end let ise_pretype_gen flags env sigma lvar kind c = - let env = make_env env sigma in + let env = GlobEnv.make env sigma lvar in let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in + let k0 = Context.Rel.length (rel_context !!env) in let c', c'_ty = match kind with | WithoutTypeConstraint -> - let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in + let j = pretype k0 flags.use_typeclasses empty_tycon env evdref c in j.uj_val, j.uj_type | OfType exptyp -> - let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in + let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref c in j.uj_val, j.uj_type | IsType -> - let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in + let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref c in tj.utj_val, mkSort tj.utj_type in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty) + process_inference_flags flags !!env sigma (!evdref,c',c'_ty) let default_inference_flags fail = { use_typeclasses = true; @@ -1236,7 +1081,7 @@ let understand_ltac flags env sigma lvar kind c = (sigma, c) let pretype k0 resolve_tc typcon env evdref lvar t = - pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t + pretype k0 resolve_tc typcon (GlobEnv.make env !evdref lvar) evdref t let pretype_type k0 resolve_tc valcon env evdref lvar t = - pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t + pretype_type k0 resolve_tc valcon (GlobEnv.make env !evdref lvar) evdref t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 73f5b77e0e..fcc361b16b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -122,11 +122,3 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types - -(**/**) - -(** To embed constr in glob_constr *) - -val register_constr_interp0 : - ('r, 'g, 't) Genarg.genarg_type -> - (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 5da5aff449..d0359b43f4 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -32,6 +32,7 @@ Program Coercion Detyping Indrec +GlobEnv Cases Pretyping Unification diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ba40262815..f133eb9963 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -628,6 +628,18 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None +let strong_with_flags whdfun flags env sigma t = + let push_rel_check_zeta d env = + let open CClosure.RedFlags in + let d = match d with + | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) + | d -> d in + push_rel d env in + let rec strongrec env t = + map_constr_with_full_binders sigma + push_rel_check_zeta strongrec env (whdfun flags env sigma t) in + strongrec env t + let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 07eeec9276..dd3cd26f0f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -144,6 +144,9 @@ val pr_state : state -> Pp.t (** {6 Reduction Function Operators } *) +val strong_with_flags : + (CClosure.RedFlags.reds -> reduction_function) -> + (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function val local_strong : local_reduction_function -> local_reduction_function val strong_prodspine : local_reduction_function -> local_reduction_function diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1810cc6588..9ed985195f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -902,28 +902,28 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = Printer.pr_global v.coe_value +let print_coercion_value v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path env sigma ((i,j),p) = +let print_path ((i,j),p) = hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j let _ = Classops.install_path_printer print_path -let print_graph env sigma = - prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) +let print_graph () = + prlist_with_sep fnl print_path (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) -let print_coercions env sigma = - pr_sequence (print_coercion_value env sigma) (coercions()) +let print_coercions () = + pr_sequence print_coercion_value (coercions()) let index_of_class cl = try @@ -932,7 +932,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between env sigma cls clt = +let print_path_between cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -943,7 +943,7 @@ let print_path_between env sigma cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path env sigma ((i,j),p) + print_path ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 1668bce297..58606db019 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +39,10 @@ val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : env -> evar_map -> Pp.t +val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 629b77be2a..44685d2bbd 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -52,7 +52,7 @@ let whd_cbn flags env sigma t = Reductionops.Stack.zip ~refold:true sigma state let strong_cbn flags = - strong (whd_cbn flags) + strong_with_flags whd_cbn flags let simplIsCbn = ref (false) let _ = Goptions.declare_bool_option { diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2170477938..85babd922b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -168,7 +168,8 @@ let classify_vernac e = | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ diff --git a/test-suite/Makefile b/test-suite/Makefile index b8aac8b6f8..f5ec80bcfc 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ - prerequisite/bind_univs.v.log + prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \ + prerequisite/module_bug7192.v.log ####################################################################### # Phony targets diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v new file mode 100644 index 0000000000..f36f757f10 --- /dev/null +++ b/test-suite/bugs/closed/8270.v @@ -0,0 +1,15 @@ +(* Don't do zeta in cbn when not asked for *) + +Goal let x := 0 in + let y := x in + y = 0. + (* We use "cofix" as an example because there are obviously no + cofixpoints in sight. This problem arises with any set of + reduction flags (not including zeta where the lets are of course reduced away) *) + cbn cofix. + intro x. + unfold x at 1. (* Should succeed *) + Undo 2. + cbn zeta. + Fail unfold x at 1. +Abort. diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v new file mode 100644 index 0000000000..0350be9c06 --- /dev/null +++ b/test-suite/bugs/closed/8288.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Set Polymorphic Inductive Cumulativity. + +Inductive foo := C : (forall A : Type -> Type, A Type) -> foo. +(* anomaly invalid subtyping relation *) diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index bd9240476f..b67ac4f0df 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -10,6 +10,8 @@ Arguments Nat.sub !n !m. About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. Delimit Scope foo_scope with F. Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. About pf. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -76,6 +76,7 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. +Declare Scope znat_scope. Delimit Scope znat_scope with znat. Open Scope znat_scope. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 34f44cd246..3f4d5ef58c 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -20,3 +20,5 @@ Axioms: M.foo : False Closed under the global context Closed under the global context +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index ea1ab63786..3d4dfe603d 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -137,3 +137,13 @@ Module F (X : T). End F. End SUBMODULES. + +(* Testing a variant of #7192 across files *) +(* This was missing in the original fix to #7192 *) +Require Import module_bug7192. +Print Assumptions M7192.D.f. + +(* Testing reporting assumptions from modules in files *) +(* A regression introduced in the original fix to #7192 was missing implementations *) +Require Import module_bug8416. +Print Assumptions M8416.f. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index eb9f571022..efdc94fb1e 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -38,3 +38,14 @@ Ltac foo := let w := () in let z := 1 in pose v +2 subgoals + + n : nat + ============================ + (fix a (n0 : nat) : nat := match n0 with + | 0 => 0 + | S n1 => a n1 + end) n = n + +subgoal 2 is: + forall a : nat, a = 0 diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 901b1e3aa6..40e743c3f0 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -71,3 +71,13 @@ Ltac foo := let z := 1 in pose v. Print Ltac foo. + +(* Ltac renaming was not applied to "fix" and "cofix" *) + +Goal forall a, a = 0. +match goal with +|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n) +end. +intro. +Show. +Abort. diff --git a/test-suite/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v new file mode 100644 index 0000000000..82cfe560af --- /dev/null +++ b/test-suite/prerequisite/module_bug7192.v @@ -0,0 +1,9 @@ +(* Variant of #7192 to be tested in a file requiring this file *) +(* #7192 is about Print Assumptions not entering implementation of submodules *) + +Definition a := True. +Module Type B. Axiom f : Prop. End B. +Module Type C. Declare Module D : B. End C. +Module M7192: C. + Module D <: B. Definition f := a. End D. +End M7192. diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v new file mode 100644 index 0000000000..70f43d132a --- /dev/null +++ b/test-suite/prerequisite/module_bug8416.v @@ -0,0 +1,2 @@ +Module Type A. Axiom f : True. End A. +Module M8416 : A. Definition f := I. End M8416. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 0f22a1f0a0..4404ff3f16 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -348,3 +348,32 @@ symmetry in H. match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *) exact (eq_refl H0). Abort. + +(* Check that internal names used in "match" compilation to push "term + to match" on the environment are not interpreted as ltac variables *) + +Module ToMatchNames. +Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac. +Goal True. +g 1. +Abort. +End ToMatchNames. + +(* An example where internal names used to build the return predicate + (here "n" because "a" is bound to "nil" and "n" is the first letter + of "nil") by small inversion should be taken distinct from Ltac names. *) + +Module LtacNames. +Inductive t (A : Type) : nat -> Type := + nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n). + +Ltac f a n := + let x := constr:(match a with nil _ => true | cons _ _ _ _ => I end) in + assert (x=x/\n=n). + +Goal forall (y:t nat 0), True. +intros. +f y true. +Abort. + +End LtacNames. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66a82008d8..42af3583d4 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -757,6 +757,8 @@ Qed. with lazy behavior (for vm_compute) *) (*****************************************) +Declare Scope lazy_bool_scope. + Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : lazy_bool_scope. Notation "a ||| b" := (if a then true else b) diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index 03e611f549..c376efef2e 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : crelation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 09b35ca75d..97510578ae 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -87,6 +87,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5217aedb88..516ea12099 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : relation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1858ba76ae..001b7dfdfd 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -88,6 +88,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 2ab3af2029..86a3a88be9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -357,6 +357,8 @@ Definition predicate_implication {l : Tlist} := (** Notations for pointwise equivalence and implication of predicates. *) +Declare Scope predicate_scope. + Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 3485b9c68d..b0d1824827 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -25,6 +25,7 @@ Unset Strict Implicit. (** Notations and helper lemma about pairs *) +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 3452967821..c0db8646c7 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -27,7 +27,7 @@ *) -Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia. Set Implicit Arguments. Unset Strict Implicit. @@ -39,7 +39,7 @@ Import Raw.Proofs. Local Open Scope pair_scope. Local Open Scope Int_scope. -Ltac omega_max := i2z_refl; romega with Z. +Ltac omega_max := i2z_refl; lia. Section Elt. Variable elt : Type. @@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: end. Proof. intros; unfold cardinal_e_2; simpl; - abstract (do 2 rewrite cons_cardinal_e; romega with * ). + abstract (do 2 rewrite cons_cardinal_e; lia ). Defined. Definition Cmp c := diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1e6843d511..76c39f275d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -37,8 +37,8 @@ Inductive bool : Set := Add Printing If bool. +Declare Scope bool_scope. Delimit Scope bool_scope with bool. - Bind Scope bool_scope with bool. (** Basic boolean operators *) @@ -136,6 +136,7 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. Arguments S _%nat. @@ -228,10 +229,13 @@ Inductive list (A : Type) : Type := Arguments nil {A}. Arguments cons {A} a l. -Infix "::" := cons (at level 60, right associativity) : list_scope. + +Declare Scope list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. +Infix "::" := cons (at level 60, right associativity) : list_scope. + Local Open Scope list_scope. Definition length (A : Type) : list A -> nat := diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 1ff00ec11c..537400fb05 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,8 +42,11 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). +Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. Bind Scope dec_uint_scope with uint. + +Declare Scope dec_int_scope. Delimit Scope dec_int_scope with int. Bind Scope dec_int_scope with int. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 72073bb4f6..8f8e639187 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -108,13 +108,17 @@ End IfNotations. (** Scopes *) -Delimit Scope type_scope with type. -Delimit Scope function_scope with function. +Declare Scope core_scope. Delimit Scope core_scope with core. -Bind Scope type_scope with Sortclass. +Declare Scope function_scope. +Delimit Scope function_scope with function. Bind Scope function_scope with Funclass. +Declare Scope type_scope. +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. + Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6afba29a0..db8857df64 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -697,7 +697,7 @@ End Choice_lemmas. Section Dependent_choice_lemmas. - Variables X : Set. + Variable X : Set. Variable R : X -> X -> Prop. Lemma dependent_choice : diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index b966f217aa..aec88f93bf 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -340,6 +340,8 @@ Functional Scheme union_ind := Induction for union Sort Prop. (** Notations and helper lemma about pairs and triples *) +Declare Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 3ba9d1f5ed..7b6740e94b 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -23,6 +23,7 @@ Inductive positive : Set := | xO : positive -> positive | xH : positive. +Declare Scope positive_scope. Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. Arguments xO _%positive. @@ -37,6 +38,7 @@ Inductive N : Set := | N0 : N | Npos : positive -> N. +Declare Scope N_scope. Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. @@ -53,6 +55,7 @@ Inductive Z : Set := | Zpos : positive -> Z | Zneg : positive -> Z. +Declare Scope Z_scope. Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index ec480bb1eb..4a1f24b95e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -21,7 +21,7 @@ Require Import Znumtheory. Require Import Zgcd_alt. Require Import Zpow_facts. Require Import CyclicAxioms. -Require Import ROmega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -1237,7 +1237,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq. destruct Z.compare; intros; @@ -1261,7 +1261,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y+1) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq. destruct Z.compare; intros; @@ -1299,8 +1299,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y) 0). rewrite <- (Z_mod_plus_full (X-Y) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq. destruct Z.compare; intros; @@ -1318,8 +1318,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y-1) 0). rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq. destruct Z.compare; intros; @@ -1356,7 +1356,7 @@ Section Int31_Specs. change [|1|] with 1; change [|0|] with 0. rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB). rewrite Zminus_mod_idemp_l. - rewrite Zmod_small; generalize (phi_bounded x); romega. + rewrite Zmod_small; generalize (phi_bounded x); lia. Qed. Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 39af62c32f..77ab624ca5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,8 +15,6 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. -Declare ML Module "int31_syntax_plugin". - (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer @@ -50,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31. Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d7f25a6613..a70ecd19d8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem - [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ] + [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ] The outcome of the modulo function is hence always positive. This corresponds to convention "E" in the following paper: @@ -46,6 +46,7 @@ Module ZEuclidProp (** We put notations in a scope, to avoid warnings about redefinitions of notations *) + Declare Scope euclid. Infix "/" := D.div : euclid. Infix "mod" := D.modulo : euclid. Local Open Scope euclid. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 3d0c005fd1..acebfcf1d2 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -220,8 +220,10 @@ End NZDomainProp. Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. + +Declare Scope ofnat. Local Open Scope ofnat. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. Lemma ofnat_zero : [O] == 0. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f55093ed48..c2316689fc 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) := Hint Unfold compose. +Declare Scope program_scope. + Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bc83881849..edbae6534a 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -326,7 +326,7 @@ Ltac program_solve_wf := Create HintDb program discriminated. -Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf. +Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 78c36dc7d1..c51cacac68 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -20,12 +20,13 @@ Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) (x ident, y ident, at level 10) : type_scope. +Declare Scope program_scope. +Delimit Scope program_scope with prg. + (** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _) : program_scope. -Delimit Scope program_scope with prg. - (** Abbreviation for first projection and hiding of proofs of subset objects. *) Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 35706e7fa2..139c4bf432 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -18,6 +18,7 @@ Require Export Morphisms Setoid Bool. Record Q : Set := Qmake {Qnum : Z; Qden : positive}. +Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 1510a7b825..81c318138e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec. Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. +Declare Scope Qc_scope. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 36ac738ca6..9f8039ec9d 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -28,6 +28,7 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x. Definition comp f1 f2 (x:R) : R := f1 (f2 x). Definition inv_fct f (x:R) : R := / f x. +Declare Scope Rfun_scope. Delimit Scope Rfun_scope with F. Arguments plus_fct (f1 f2)%F x%R. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 6019d4faf1..a2818371e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,6 +14,7 @@ Require Export ZArith_base. Require Export Rdefinitions. +Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 857b4ec33b..932fcddaf5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,12 +12,15 @@ (** Definitions for the axiomatization *) (*********************************************************) -Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. -(* Declare Scope positive_scope with Key R *) +(* Declare primitive numeral notations for Scope R_scope *) +Declare Scope R_scope. +Declare ML Module "r_syntax_plugin". + +(* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 31a7fb8ad6..3f676c1888 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,7 +13,6 @@ Adapted to Coq V8 by the Coq Development Team *) Require Import Bool BinPos BinNat PeanoNat Nnat. -Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin". Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). +Declare Scope char_scope. +Declare ML Module "ascii_syntax_plugin". Delimit Scope char_scope with char. Bind Scope char_scope with ascii. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index be9a10c6dc..b27474ef25 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,7 +15,6 @@ Require Import Arith. Require Import Ascii. Require Import Bool. -Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) @@ -25,6 +24,8 @@ Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. +Declare Scope string_scope. +Declare ML Module "string_syntax_plugin". Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 87df6b479d..60c64d306b 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType'). Module OrderTac := OT_to_OrderTac O. Ltac order := OrderTac.order. + Declare Scope order. Notation "x <= y" := (~lt y x) : order. Infix "?=" := compare (at level 70, no associativity) : order. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index ba3e411091..390ca78c0e 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -305,6 +305,7 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni End VECTORLIST. Module VectorNotations. +Declare Scope vector_scope. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 2f3bf9a32a..1e35370d29 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -17,6 +17,7 @@ *) Require Import BinInt. +Declare Scope Int_scope. Delimit Scope Int_scope with I. Local Open Scope Int_scope. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index e93ebb1ad5..0c9aca2657 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. +Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. @@ -129,33 +129,33 @@ Qed. Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. @@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - - romega with *. - - romega with *. - - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - lia. + - lia. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } - destruct r; simpl Z.sgn in *; romega with *. + destruct r; simpl Z.sgn in *; lia. Qed. Theorem Zquot_mod_unique_full a b q r : @@ -185,7 +185,7 @@ Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. - romega with *. + lia. rewrite <- H1; apply Z.quot_rem'. rewrite <- (Z.opp_involutive a). @@ -193,7 +193,7 @@ Proof. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. - romega with *. + lia. Qed. Theorem Zquot_unique_full a b q r : diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 765f962e99..e5d2382e46 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with - | MPfile _ -> raise Not_found + | MPfile _ -> Global.lookup_module mp | MPbound _ -> assert false | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74516e320c..44c0159d1b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram info = hint_info -> { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + (* Should be in syntax, but camlp5 would not factorize *) + | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> + { VernacDeclareScope sc } + (* System directory *) | IDENT "Pwd" -> { VernacChdir None } | IDENT "Cd" -> { VernacChdir None } @@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> { VernacSyntaxExtension (false, (s,l)) } - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) + (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order + to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; only_parsing: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d66a121437..2e5e11bb09 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1306,8 +1306,18 @@ type notation_obj = { notobj_notation : notation * notation_location; } -let load_notation _ (_, nobj) = - Option.iter Notation.declare_scope nobj.notobj_scope +let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = + (* When the default shall be to require that a scope already exists *) + (* the call to ensure_scope will have to be removed *) + if silently_define_scope_if_undefined then + (* Don't warn if the scope is not defined: *) + (* there was already a warning at "cache" time *) + Option.iter Notation.declare_scope nobj.notobj_scope + else + Option.iter Notation.ensure_scope nobj.notobj_scope + +let load_notation = + load_notation_common true let open_notation i (_, nobj) = let scope = nobj.notobj_scope in @@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) = end let cache_notation o = - load_notation 1 o; + load_notation_common false 1 o; open_notation 1 o let subst_notation (subst, nobj) = @@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = add_notation local env c (df,modifiers) sc (**********************************************************************) -(* Delimiters and classes bound to scopes *) +(* Scopes, delimiters and classes bound to scopes *) type scope_command = - | ScopeDelim of string + | ScopeDeclare + | ScopeDelimAdd of string + | ScopeDelimRemove | ScopeClasses of scope_class list - | ScopeRemove - -let load_scope_command _ (_,(scope,dlm)) = - Notation.declare_scope scope -let open_scope_command i (_,(scope,o)) = +let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) = + let declare_scope_if_needed = + if silently_define_scope_if_undefined then Notation.declare_scope + else Notation.ensure_scope in + match o with + | ScopeDeclare -> Notation.declare_scope scope + (* When the default shall be to require that a scope already exists *) + (* the call to declare_scope_if_needed will have to be removed below *) + | ScopeDelimAdd dlm -> declare_scope_if_needed scope + | ScopeDelimRemove -> declare_scope_if_needed scope + | ScopeClasses cl -> declare_scope_if_needed scope + +let load_scope_command = + load_scope_command_common true + +let open_scope_command i (_,(local,scope,o)) = if Int.equal i 1 then match o with - | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeDeclare -> () + | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm + | ScopeDelimRemove -> Notation.remove_delimiters scope | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl - | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = - load_scope_command 1 o; + load_scope_command_common false 1 o; open_scope_command 1 o -let subst_scope_command (subst,(scope,o as x)) = match o with +let subst_scope_command (subst,(local,scope,o as x)) = match o with | ScopeClasses cl -> let cl' = List.map_filter (subst_scope_class subst) cl in let cl' = if List.for_all2eq (==) cl cl' then cl else cl' in - scope, ScopeClasses cl' + local, scope, ScopeClasses cl' | _ -> x -let inScopeCommand : scope_name * scope_command -> obj = +let classify_scope_command (local, _, _ as o) = + if local then Dispose else Substitute o + +let inScopeCommand : locality_flag * scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj)} + classify_function = classify_scope_command} + +let declare_scope local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare)) -let add_delimiters scope key = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let add_delimiters local scope key = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key)) -let remove_delimiters scope = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) +let remove_delimiters local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove)) -let add_class_scope scope cl = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) +let add_class_scope local scope cl = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 73bee7121b..38dbdf7e41 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr -> val add_notation_extra_printing_rule : string -> string -> string -> unit -(** Declaring delimiter keys and default scopes *) +(** Declaring scopes, delimiter keys and default scopes *) -val add_delimiters : scope_name -> string -> unit -val remove_delimiters : scope_name -> unit -val add_class_scope : scope_name -> scope_class list -> unit +val declare_scope : locality_flag -> scope_name -> unit +val add_delimiters : locality_flag -> scope_name -> string -> unit +val remove_delimiters : locality_flag -> scope_name -> unit +val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 93e4e89a12..63e9e4fe49 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -635,6 +635,10 @@ open Pputils keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) + | VernacDeclareScope sc -> + return ( + keyword "Declare Scope" ++ spc () ++ str sc + ) | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f7ba305374..681dce3ca3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -403,17 +403,24 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension atts infix l = +let vernac_syntax_extension ~atts infix l = let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l -let vernac_delimiters sc = function - | Some lr -> Metasyntax.add_delimiters sc lr - | None -> Metasyntax.remove_delimiters sc +let vernac_declare_scope ~atts sc = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_scope local sc + +let vernac_delimiters ~atts sc action = + let local = enforce_module_locality atts.locality in + match action with + | Some lr -> Metasyntax.add_delimiters local sc lr + | None -> Metasyntax.remove_delimiters local sc -let vernac_bind_scope sc cll = - Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) +let vernac_bind_scope ~atts sc cll = + let local = enforce_module_locality atts.locality in + Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll) let vernac_open_close_scope ~atts (b,s) = let local = enforce_section_locality atts.locality in @@ -1802,13 +1809,13 @@ let vernac_print ~atts env sigma = | PrintName (qid,udecl) -> dump_global qid; print_name env sigma qid udecl - | PrintGraph -> Prettyp.print_graph env sigma + | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() | PrintInstances c -> Prettyp.print_instances (smart_global c) - | PrintCoercions -> Prettyp.print_coercions env sigma + | PrintCoercions -> Prettyp.print_coercions () | PrintCoercionPaths (cls,clt) -> - Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -2093,9 +2100,10 @@ let interp ?proof ~atts ~st c = (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - vernac_syntax_extension atts infix sl - | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr - | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl + vernac_syntax_extension ~atts infix sl + | VernacDeclareScope sc -> vernac_declare_scope ~atts sc + | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr + | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> @@ -2232,6 +2240,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _ | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8fb74e6d78..11b2a7d802 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -325,6 +325,7 @@ type nonrec vernac_expr = (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name + | VernacDeclareScope of scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of (lstring * syntax_modifier list) * |