diff options
68 files changed, 536 insertions, 303 deletions
diff --git a/.gitattributes b/.gitattributes index db179c8d20..e087e17379 100644 --- a/.gitattributes +++ b/.gitattributes @@ -19,6 +19,7 @@ tools/CoqMakefile.in whitespace=trailing-space *.css whitespace=trailing-space,tab-in-indent *.dtd whitespace=trailing-space,tab-in-indent *.el whitespace=trailing-space,tab-in-indent +*.g whitespace=trailing-space,tab-in-indent *.h whitespace=trailing-space,tab-in-indent *.html whitespace=trailing-space,tab-in-indent *.hva whitespace=trailing-space,tab-in-indent @@ -37,9 +38,11 @@ tools/CoqMakefile.in whitespace=trailing-space *.nsh whitespace=trailing-space,tab-in-indent *.nsi whitespace=trailing-space,tab-in-indent *.py whitespace=trailing-space,tab-in-indent +*.rst whitespace=trailing-space,tab-in-indent *.sh whitespace=trailing-space,tab-in-indent *.sty whitespace=trailing-space,tab-in-indent *.tex whitespace=trailing-space,tab-in-indent +*.tokens whitespace=trailing-space,tab-in-indent *.txt whitespace=trailing-space,tab-in-indent *.v whitespace=trailing-space,tab-in-indent *.xml whitespace=trailing-space,tab-in-indent diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 03e001f4a9..f0d7463fc9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -85,10 +85,6 @@ before_script: - echo 'end:coq.install' - set +e - variables: &build-variables - EXTRA_CONF: "-native-compiler yes -coqide opt" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM" .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur @@ -151,9 +147,9 @@ before_script: build: <<: *build-template variables: - EXTRA_CONF: "-with-doc yes" - EXTRA_PACKAGES: "$COQDOC_PACKAGES" - EXTRA_OPAM: "$COQDOC_OPAM" + EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" + EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES" + EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM" PIP_PACKAGES: "$SPHINX_PACKAGES" # no coqide for 32bit: libgtk installation problems @@ -167,9 +163,10 @@ build:32bit: build:bleeding-edge: <<: *build-template variables: - <<: *build-variables + EXTRA_CONF: "-native-compiler yes -coqide opt" COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM_BE" warnings: @@ -6,6 +6,15 @@ Tools - Coq_makefile lets one override or extend the following variables from the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. +Vernacular Commands + +- Removed deprecated commands Arguments Scope and Implicit Arguments + (not the option). Use the Arguments command instead. + +Tactic language + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + Changes from 8.7.2 to 8.8+beta1 =============================== diff --git a/clib/cArray.ml b/clib/cArray.ml index b6c033f6d2..5eb20bc169 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -41,6 +41,8 @@ sig ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left4 : + ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a val fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a @@ -267,6 +269,16 @@ let fold_left3 f a v1 v2 v3 = invalid_arg "Array.fold_left2"; fold a 0 +let fold_left4 f a v1 v2 v3 v4 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a + else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n) + in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then + invalid_arg "Array.fold_left4"; + fold a 0 + let fold_left_from n f a v = let len = Array.length v in let () = if n < 0 then invalid_arg "Array.fold_left_from" in diff --git a/clib/cArray.mli b/clib/cArray.mli index 97038b0ac2..f4f60f8aa4 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -66,6 +66,8 @@ sig ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left4 : + ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a val fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4e8c7e145e..4f7e9517f4 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -11,25 +11,6 @@ wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v -# Delete useless calls to try omega; unfold -patch vfa/SearchTree.v <<EOF -*** SearchTree.v.bak 2017-09-06 19:12:59.000000000 +0200 ---- SearchTree.v 2017-11-21 16:34:41.000000000 +0100 -*************** -*** 674,683 **** - forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j. - Proof. - intros. -- try omega. (* Oops! [omega] cannot solve this one. -- The problem is that [i] and [j] have type [key] instead of type [nat]. -- The solution is easy enough: *) -- unfold key in *. - omega. - - (** So, if you get stuck on an [omega] that ought to work, ---- 674,679 ---- -EOF - ( cd lf && make clean && make ) ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ee9c8777a3..cd09b6d305 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -31,4 +31,6 @@ fi find . "(" -path ./.git -prune ")" -o -type f -print0 | xargs -0 dev/tools/check-eof-newline.sh || CODE=1 +dev/tools/check-overlays.sh || CODE=1 + exit $CODE diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh new file mode 100755 index 0000000000..f7e05b51cd --- /dev/null +++ b/dev/tools/check-overlays.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +for f in dev/ci/user-overlays/* +do + if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]]) + then + >&2 echo "Bad overlay '$f'." + >&2 echo "User overlays need to have extension .sh to be picked up!" + exit 1 + fi +done diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index c9cdee84ab..a514b8866a 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,6 +5,8 @@ set -e +dev/tools/check-overlays.sh + if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; then diff --git a/engine/proofview.ml b/engine/proofview.ml index 22271dd02c..639f48e77c 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -710,13 +710,19 @@ let partition_unifiable sigma l = (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered). *) -let shelve_unifiable = +let shelve_unifiable_informative = let open Proof in Pv.get >>= fun initial -> let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ CList.map drop_state u) + let u = CList.map drop_state u in + Shelf.modify (fun gls -> gls @ u) >> + tclUNIT u + +let shelve_unifiable = + let open Proof in + shelve_unifiable_informative >>= fun _ -> tclUNIT () (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -1035,6 +1041,8 @@ module Unsafe = struct let advance = Evarutil.advance + let undefined = undefined + let mark_as_unresolvable p gl = { p with solution = mark_in_evm ~goal:false p.solution gl } diff --git a/engine/proofview.mli b/engine/proofview.mli index e7be665527..1905686fe7 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -326,6 +326,9 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool considered). *) val shelve_unifiable : unit tactic +(** Idem but also returns the list of shelved variables *) +val shelve_unifiable_informative : Evar.t list tactic + (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) val guard_no_unifiable : Names.Name.t list option tactic @@ -466,6 +469,12 @@ module Unsafe : sig solved. *) val advance : Evd.evar_map -> Evar.t -> Evar.t option + (** [undefined sigma l] applies [advance] to the goals of [l], then + returns the subset of resulting goals which have not yet been + defined *) + val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> + Proofview_monad.goal_with_state list + val typeclass_resolvable : unit Evd.Store.field end diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19444988b9..48ddd94961 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -14,7 +14,6 @@ open CErrors open Util open Names open Nameops -open Constr open Termops open Libnames open Globnames @@ -1223,8 +1222,36 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + | PFix ((ln,i),(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let n = Array.length tl in + let v = Array.map3 + (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) + bl tl ln in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + | PCoFix (ln,(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let ntys = Array.length tl in + let v = Array.map2 + (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t)) + bl tl in + GRec(GCoFix ln,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) | PSort s -> GSort s let extern_constr_pattern env sigma pat = diff --git a/intf/pattern.ml b/intf/pattern.ml index af2347674f..76367b612a 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -10,7 +10,6 @@ open Names open Globnames -open Constr open Misctypes (** {5 Patterns} *) @@ -37,8 +36,8 @@ type constr_pattern = | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * (int * bool list * constr_pattern) list (** index of constructor, nb of args *) - | PFix of fixpoint - | PCoFix of cofixpoint + | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) + | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index dc1110ad86..96b4a0e26f 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -409,8 +409,6 @@ type nonrec vernac_expr = | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacDeclareImplicits of reference or_by_notation * - (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * @@ -418,8 +416,6 @@ type nonrec vernac_expr = [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list - | VernacArgumentsScope of reference or_by_notation * - scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8543d2b849..7114e6c583 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -601,14 +601,6 @@ GEXTEND Gram ; END -let warn_deprecated_arguments_scope = - CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" - (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") - -let warn_deprecated_implicit_arguments = - CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" - (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") - (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name hint_info; @@ -691,20 +683,6 @@ GEXTEND Gram let more_implicits = Option.default [] more_implicits in VernacArguments (qid, args, more_implicits, !slash_position, mods) - - (* moved there so that camlp5 factors it with the previous rule *) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warn_deprecated_arguments_scope ~loc:!@loc (); - VernacArgumentsScope (qid,scl) - - (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> - List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warn_deprecated_implicit_arguments ~loc:!@loc (); - VernacDeclareImplicits (qid,pos) - | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -734,12 +712,6 @@ GEXTEND Gram [`ClearImplicits; `ClearScopes] ] ] ; - implicit_name: - [ [ "!"; id = ident -> (id, false, true) - | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) - | "["; id = ident; "]" -> (id,true, false) ] ] - ; scope: [ [ "%"; key = IDENT -> key ] ] ; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 888c76e3d9..89d490a410 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -183,9 +183,36 @@ let push_binder na1 na2 t ctx = Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx -let to_fix (idx, (nas, cs, ts)) = - let inj = EConstr.of_constr in - (idx, (nas, Array.map inj cs, Array.map inj ts)) +(* This is an optimization of the main pattern-matching which shares + the longest common prefix of the body and type of a fixpoint. The + only practical effect at the time of writing is in binding variable + names: these variable names must be bound only once since the user + view at a fix displays only a (maximal) shared common prefix *) + +let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 = + match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with + | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') -> + let ctx = push_binder na1 na2 c2 ctx in + let ctx' = push_binder na1 na2' c2' ctx' in + let env = EConstr.push_rel (LocalAssum (na2,c2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1' t2' b1' b2' + | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) -> + let ctx = push_binder na1 na2 u2 ctx in + let ctx' = push_binder na1 na2' u2' ctx' in + let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in + let subst = sorec ctx env subst c1 c2 in + let subst = sorec ctx env subst c1' c2' in + let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in + let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in + let subst = add_binders na1 na2 binding_vars subst in + match_under_common_fix_binders sorec sigma binding_vars + ctx ctx' env env' subst t1 t2 b1 b2 + | _ -> + sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2 let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with @@ -364,8 +391,20 @@ let matches_core env sigma allow_bound_rels let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in List.fold_left chk_branch chk_head br1 - | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst - | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) + when Array.equal Int.equal ln1 ln2 && i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + + | PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2)) + when i1 = i2 -> + let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in + let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in + let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in + Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2 + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> Array.fold_left2 (sorec ctx env) subst args1 args2 | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 587892141c..bb563220b6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let rec share_names detype n l avoid env sigma c t = + match EConstr.kind sigma c, EConstr.kind sigma t with + (* factorize even when not necessary to have better presentation *) + | Lambda (na,t,c), Prod (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in + share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + (* May occur for fix built interactively *) + | LetIn (na,b,t',c), _ when n > 0 -> + let t'' = detype avoid env sigma t' in + let b' = detype avoid env sigma b in + let id = next_name_away na avoid in + let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in + share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + (* Only if built with the f/n notation or w/o let-expansion in types *) + | _, LetIn (_,b,_,t) when n > 0 -> + share_names detype n l avoid env sigma c (subst1 b t) + (* If it is an open proof: we cheat and eta-expand *) + | _, Prod (na',t',c') when n > 0 -> + let t'' = detype avoid env sigma t' in + let id = next_name_away na' avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in + let appc = mkApp (lift 1 c,[|mkRel 1|]) in + share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + (* If built with the f/n notation: we renounce to share names *) + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let rec share_pattern_names detype n l avoid env sigma c t = + let open Pattern in + if n = 0 then + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + else match c, t with + | PLambda (na,t,c), PProd (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid in + let env = Name id :: env in + share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let n = Array.length tys in + let v = Array.map3 + (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t)) + bodies tys vn in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + +let detype_cofix detype avoid env sigma n (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let ntys = Array.length tys in + let v = Array.map2 + (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t)) + bodies tys in + GRec(GCoFix n,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + let detype_universe sigma u = let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in Univ.Universe.map fn u @@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t = (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) p c bl - | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef - -and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let n = Array.length tys in - let v = Array.map3 - (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) - bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and detype_cofix d flags avoid env sigma n (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let ntys = Array.length tys in - let v = Array.map2 - (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) - bodies tys in - GRec(GCoFix n,Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and share_names d flags n l avoid env sigma c t = - match EConstr.kind sigma c, EConstr.kind sigma t with - (* factorize even when not necessary to have better presentation *) - | Lambda (na,t,c), Prod (na',t',c') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in - let t' = detype d flags avoid env sigma t in - let id = next_name_away na avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in - share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' - (* May occur for fix built interactively *) - | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let b' = detype d flags avoid env sigma b in - let id = next_name_away na avoid in - let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in - share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) - (* Only if built with the f/n notation or w/o let-expansion in types *) - | _, LetIn (_,b,_,t) when n > 0 -> - share_names d flags n l avoid env sigma c (subst1 b t) - (* If it is an open proof: we cheat and eta-expand *) - | _, Prod (na',t',c') when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let id = next_name_away na' avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in - let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' - (* If built with the f/n notation: we renounce to share names *) - | _ -> - if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype d flags avoid env sigma c in - let t = detype d flags avoid env sigma t in - (List.rev l,c,t) + | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 32b94e1b03..817b8ba6e8 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list +val share_pattern_names : + (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list -> + Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> + Pattern.constr_pattern -> + (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a + val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74f2cefab6..e89bbf7c34 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 - | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index dcb93bfb62..e52112fda0 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,7 +15,6 @@ open Globnames open Nameops open Term open Constr -open Vars open Glob_term open Pp open Mod_subst @@ -57,10 +56,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with constr_pattern_eq p1 p2 && constr_pattern_eq r1 r2 && List.equal pattern_eq l1 l2 -| PFix f1, PFix f2 -> - fixpoint_eq f1 f2 -| PCoFix f1, PCoFix f2 -> - cofixpoint_eq f1 f2 +| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> + Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2 +| PCoFix (i1,f1), PCoFix (i2,f2) -> + Int.equal i1 i2 && rec_declaration_eq f1 f2 | PProj (p1, t1), PProj (p2, t2) -> Projection.equal p1 p2 && constr_pattern_eq t1 t2 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ @@ -71,19 +70,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with and pattern_eq (i1, j1, p1) (i2, j2, p2) = Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 -and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) = - Int.equal i1 i2 && - Array.equal Int.equal arg1 arg2 && - rec_declaration_eq r1 r2 - -and cofixpoint_eq (i1, r1) (i2, r2) = - Int.equal i1 i2 && - rec_declaration_eq r1 r2 - and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Constr.equal c1 c2 && - Array.equal Constr.equal r1 r2 + Array.equal constr_pattern_eq c1 c2 && + Array.equal constr_pattern_eq r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -123,8 +113,10 @@ let rec occurn_pattern n = function | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> Array.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ -> false - | PFix fix -> not (noccurn n (mkFix fix)) - | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + | PFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl + | PCoFix (_,(_,tl,bl)) -> + Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl let noccurn_pattern n c = not (occurn_pattern n c) @@ -209,8 +201,16 @@ let pattern_of_constr env sigma t = in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) - | Fix f -> PFix f - | CoFix f -> PCoFix f in + | Fix (lni,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) + | CoFix (ln,(lna,tl,bl)) -> + let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in + let env' = Array.fold_left2 push env lna tl in + PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + Array.map (pattern_of_constr env') bl)) in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -225,10 +225,14 @@ let map_pattern_with_binders g f l = function | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) | PProj (p,pc) -> PProj (p, f l pc) + | PFix (lni,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | PCoFix (ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* Non recursive *) - | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ - (* Bound to terms *) - | PFix _ | PCoFix _ as x) -> x + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x let error_instantiate_pattern id l = let is = match l with @@ -262,15 +266,12 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c let rec liftn_pattern k n = function | PRel i as x -> if i >= n then PRel (i+k) else x - | PFix x -> PFix (destFix (liftn k n (mkFix x))) - | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x))) | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c let lift_pattern k = liftn_pattern k 1 @@ -337,19 +338,35 @@ let rec subst_pattern subst pat = if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') - | PFix fixpoint -> - let cstr = mkFix fixpoint in - let fixpoint' = destFix (subst_mps subst cstr) in - if fixpoint' == fixpoint then pat else - PFix fixpoint' - | PCoFix cofixpoint -> - let cstr = mkCoFix cofixpoint in - let cofixpoint' = destCoFix (subst_mps subst cstr) in - if cofixpoint' == cofixpoint then pat else - PCoFix cofixpoint' - -let mkPLambda na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambda = List.fold_right mkPLambda + | PFix (lni,(lna,tl,bl)) -> + let tl' = Array.smartmap (subst_pattern subst) tl in + let bl' = Array.smartmap (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PFix (lni,(lna,tl',bl')) + | PCoFix (ln,(lna,tl,bl)) -> + let tl' = Array.smartmap (subst_pattern subst) tl in + let bl' = Array.smartmap (subst_pattern subst) bl in + if bl' == bl && tl' == tl then pat + else PCoFix (ln,(lna,tl',bl')) + +let mkPLetIn na b t c = PLetIn(na,b,t,c) +let mkPProd na t u = PProd(na,t,u) +let mkPLambda na t b = PLambda(na,t,b) +let mkPLambdaUntyped na b = PLambda(na,PMeta None,b) +let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped + +let mkPProd_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPProd na t c + | Some b -> mkPLetIn na b (Some t) c + +let mkPLambda_or_LetIn (na,_,bo,t) c = + match bo with + | None -> mkPLambda na t c + | Some b -> mkPLetIn na b (Some t) c + +let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c) +let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c) let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp @@ -428,7 +445,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in - rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) + rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p)) | None, _ -> PMeta None | Some p, None -> match DAst.get p with @@ -450,9 +467,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GProj(p,c) -> PProj(p, pat_of_raw metas vars c) - | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + | GRec (GFix (ln,n), ids, decls, tl, cl) -> + if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then + err ?loc (Pp.str "\"struct\" annotation is expected.") + else + let ln = Array.map (fst %> Option.get) ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) + + | GRec (GCoFix n, ids, decls, tl, cl) -> + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PCoFix (n, (names, tl, cl)) + + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ -> err ?loc (Pp.str "Non supported pattern.")) +and pat_of_glob_in_context metas vars decls c = + let rec aux acc vars = function + | (na,bk,b,t) :: decls -> + let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in + aux (decl::acc) (na::vars) decls + | [] -> + acc, pat_of_raw metas vars c + in aux [] vars decls + and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with | PatVar na -> @@ -477,7 +525,7 @@ and pats_of_glob_branches loc metas vars ind brs = (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7df0a0c94a..2706893ac9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -155,13 +155,6 @@ open Decl_kinds let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_explanation (e,b,f) = - let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") - | ExplByName id -> pr_id id in - let a = if f then str"!" ++ a else a in - if b then str "[" ++ a ++ str "]" else a - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -653,16 +646,6 @@ open Decl_kinds keyword "Bind Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " @@ -1016,18 +999,6 @@ open Decl_kinds | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( diff --git a/stm/stm.mli b/stm/stm.mli index a8eb10fb33..7a720aa72a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -39,14 +39,25 @@ module AsyncOpts : sig end -(** The STM doc type determines some properties such as what - uncompleted proofs are allowed and recording of aux files. *) +(** The STM document type [stm_doc_type] determines some properties + such as what uncompleted proofs are allowed and what gets recorded + to aux files. *) type stm_doc_type = - | VoDoc of string - | VioDoc of string - | Interactive of DirPath.t + | VoDoc of string (* file path *) + | VioDoc of string (* file path *) + | Interactive of DirPath.t (* module path *) -(* Main initalization routine *) +(** Coq initalization options: + + - [doc_type]: Type of document being created. + + - [require_libs]: list of libraries/modules to be pre-loaded at + startup. A tuple [(modname,modfrom,import)] is equivalent to [From + modfrom Require modname]; [import] works similarly to + [Library.require_library_from_dirpath], [Some false] will import + the module, [Some true] will additionally export it. + +*) type stm_init_options = { (* The STM will set some internal flags differently depending on the specified [doc_type]. This distinction should dissappear at some @@ -72,12 +83,14 @@ type stm_init_options = { (** The type of a STM document *) type doc +(** [init_core] performs some low-level initalization; should go away + in future releases. *) val init_core : unit -> unit -(* Starts a new document *) +(** [new_doc opt] Creates a new document with options [opt] *) val new_doc : stm_init_options -> doc * Stateid.t -(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing +(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_control CAst.t @@ -115,14 +128,15 @@ val query : doc:doc -> type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ] -(* Evaluates the tip of the current branch *) +(* [observe doc sid]] Check / execute span [sid] *) +val observe : doc:doc -> Stateid.t -> doc + +(* [finish doc] Fully checks a document up to the "current" tip. *) val finish : doc:doc -> doc (* Internal use (fake_ide) only, do not use *) val wait : doc:doc -> doc -val observe : doc:doc -> Stateid.t -> doc - val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 9a8af3a58c..4efe1f7ba0 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -145,7 +145,7 @@ let classify_vernac e = | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacArguments _ | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 958a205a15..a97ae8f655 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -369,9 +369,36 @@ module New = struct tclTHENSFIRSTn t1 l (tclUNIT()) let tclTHENFIRST t1 t2 = tclTHENFIRSTn t1 [|t2|] + + let tclBINDFIRST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match gls with + | [] -> tclFAIL 0 (str "Expect at least one goal.") + | hd::tl -> + Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclNEWGOALS tl <*> + Proofview.tclUNIT ans + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] + + let option_of_failure f x = try Some (f x) with Failure _ -> None + + let tclBINDLAST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match option_of_failure List.sep_last gls with + | None -> tclFAIL 0 (str "Expect at least one goal.") + | Some (last,firstn) -> + Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun newgls -> + tclEVARMAP >>= fun sigma -> + let firstn = Proofview.Unsafe.undefined sigma firstn in + Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*> + Proofview.tclUNIT ans + let tclTHENS t l = tclINDEPENDENT begin t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index f0ebac780e..340d8fbf3d 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -196,8 +196,10 @@ module New : sig (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic + val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic val tclTHENLAST : unit tactic -> unit tactic -> unit tactic + val tclBINDLAST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic (* [tclTHENS t l = t <*> tclDISPATCH l] *) val tclTHENS : unit tactic -> unit tactic list -> unit tactic (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 834d73bdda..0d9f3d8216 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4987,15 +4987,15 @@ let anon_id = Id.of_string "anonymous" let name_op_to_name name_op object_kind suffix = let open Proof_global in let default_gk = (Global, false, object_kind) in + let name, gk = match Proof_global.V82.get_current_initial_conclusions () with + | (id, (_, gk)) -> Some id, gk + | exception NoCurrentProof -> None, default_gk + in match name_op with - | Some s -> - (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk - with NoCurrentProof -> s, default_gk) - | None -> - let name, gk = - try let name, gk, _ = Pfedit.current_proof_statement () in name, gk - with NoCurrentProof -> anon_id, default_gk in - add_suffix name suffix, gk + | Some s -> s, gk + | None -> + let name = Option.default anon_id name in + add_suffix name suffix, gk let tclABSTRACT ?(opaque=true) name_op tac = let s, gk = if opaque diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v index 8c5a38859f..79a0a14d7c 100644 --- a/test-suite/bugs/closed/1341.v +++ b/test-suite/bugs/closed/1341.v @@ -8,7 +8,7 @@ Hypothesis Xst : forall A, Equivalence (Xeq A). Variable map : forall A B, (A -> B) -> X A -> X B. -Implicit Arguments map [A B]. +Arguments map [A B]. Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c). intros A B a b c f Hab Hbc. diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v index 17eeb35291..c41e45900a 100644 --- a/test-suite/bugs/closed/1844.v +++ b/test-suite/bugs/closed/1844.v @@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. -Implicit Arguments update [A]. +Arguments update [A]. Definition ident := Z. Parameter operator: Set. diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v index 685811176a..5024a5bc97 100644 --- a/test-suite/bugs/closed/1891.v +++ b/test-suite/bugs/closed/1891.v @@ -3,7 +3,7 @@ Definition f (A: Set) (l: T A): unit := tt. - Implicit Arguments f [A]. + Arguments f [A]. Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v index 7558b0b86d..e950554c4b 100644 --- a/test-suite/bugs/closed/1951.v +++ b/test-suite/bugs/closed/1951.v @@ -42,7 +42,7 @@ match s as a return (S a) with pair (ind2 a0) IHl) l) end. (* some induction principle *) -Implicit Arguments ind [S]. +Arguments ind [S]. Lemma k : a -> Type. (* some ininteresting lemma *) intro;pattern H;apply ind;intros. diff --git a/test-suite/bugs/closed/1981.v b/test-suite/bugs/closed/1981.v index 99952682d5..a3d9429307 100644 --- a/test-suite/bugs/closed/1981.v +++ b/test-suite/bugs/closed/1981.v @@ -1,4 +1,4 @@ -Implicit Arguments ex_intro [A]. +Arguments ex_intro [A]. Goal exists n : nat, True. eapply ex_intro. exact 0. exact I. diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v index febb9c7bb0..10e86cd12d 100644 --- a/test-suite/bugs/closed/2362.v +++ b/test-suite/bugs/closed/2362.v @@ -8,7 +8,7 @@ Class Pointed (M:Type -> Type) := Unset Implicit Arguments. Inductive FPair (A B:Type) (neutral: B) : Type:= fpair : forall (a:A) (b:B), FPair A B neutral. -Implicit Arguments fpair [[A] [B] [neutral]]. +Arguments fpair {A B neutral}. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 23a58501f3..6d73d58d4e 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -63,7 +63,7 @@ Fixpoint lpSat st f: Prop := end. End PropLogic. -Implicit Arguments lpSat. +Arguments lpSat : default implicits. Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := match f with @@ -71,7 +71,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) end. -Implicit Arguments LPTransfo. +Arguments LPTransfo : default implicits. Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f. @@ -139,7 +139,7 @@ Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) := fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)). -Implicit Arguments trProd. +Arguments trProd : default implicits. Require Import Setoid. Theorem satTrProd: diff --git a/test-suite/bugs/closed/2404.v b/test-suite/bugs/closed/2404.v index 8ac696e912..f6ec676014 100644 --- a/test-suite/bugs/closed/2404.v +++ b/test-suite/bugs/closed/2404.v @@ -22,13 +22,13 @@ Section Derived. Definition bexportw := exportw base. Definition bwweak := wweak base. - Implicit Arguments bexportw [a b]. + Arguments bexportw [a b]. Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type := starReflS : forall a, RstarSetProof T a a | starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k. -Implicit Arguments starTransS [I T i j k]. +Arguments starTransS [I T i j k]. Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))). diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v index ef2e4e3555..b5a723b47f 100644 --- a/test-suite/bugs/closed/2584.v +++ b/test-suite/bugs/closed/2584.v @@ -8,7 +8,7 @@ Inductive res (A: Type) : Type := | OK: A -> res A | Error: err -> res A. -Implicit Arguments Error [A]. +Arguments Error [A]. Set Printing Universes. diff --git a/test-suite/bugs/closed/2667.v b/test-suite/bugs/closed/2667.v index 0631e5358d..0e6d0108cc 100644 --- a/test-suite/bugs/closed/2667.v +++ b/test-suite/bugs/closed/2667.v @@ -1,11 +1,11 @@ -(* Check that extra arguments to Arguments Scope do not disturb use of *) +(* Check that extra arguments to Arguments do not disturb use of *) (* scopes in constructors *) Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt. Bind Scope Cminor with stmt. (* extra argument is ok because of possible coercion to funclass *) -Arguments Scope Scall [_ Cminor ]. +Arguments Scall _ _%Cminor : extra scopes. (* extra argument is ok because of possible coercion to funclass *) Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end. diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v index 7929b88108..c9d65c12c7 100644 --- a/test-suite/bugs/closed/2729.v +++ b/test-suite/bugs/closed/2729.v @@ -82,8 +82,8 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Implicit Arguments Nil [pu cxt]. -Implicit Arguments Cons [pu from mid to]. +Arguments Nil [pu cxt]. +Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} {from mid to : NameSet} diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index bb607b785b..07a5cf91a5 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -49,9 +49,9 @@ Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := ; af_level2 : forall x y, age1 x = Some y -> level x = S (level y) }. -Implicit Arguments af_unage [[A] [level] [age1]]. -Implicit Arguments af_level1 [[A] [level] [age1]]. -Implicit Arguments af_level2 [[A] [level] [age1]]. +Arguments af_unage {A level age1}. +Arguments af_level1 {A level age1}. +Arguments af_level2 {A level age1}. Class ageable (A:Type) := mkAgeable { level : A -> nat @@ -77,7 +77,7 @@ Coercion app_pred : pred >-> Funclass. Global Opaque pred. Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a. -Implicit Arguments derives. +Arguments derives : default implicits. Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A := fun a:A => P a /\ Q a. @@ -170,7 +170,7 @@ Class Functor `(C:Category) `(D:Category) (im : C -> D) := { fmap g ∘ fmap f ≈ fmap (g ∘ f) }. Coercion functor_im : Functor >-> Funclass. -Implicit Arguments fmap [Object Hom C Object0 Hom0 D im a b]. +Arguments fmap [Object Hom C Object0 Hom0 D im] _ [a b]. Add Parametric Morphism `(C:Category) `(D:Category) (Im:C->D) (F:Functor C D Im) (a b:C) : (@fmap _ _ C _ _ D Im F a b) diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index 79671ce930..9811733dc6 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -33,7 +33,7 @@ Section Counted_list. End Counted_list. -Implicit Arguments counted_def_nth [A n]. +Arguments counted_def_nth [A n]. Section Finite_nat_set. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 1f0f3b0da9..a1d0b9107b 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -21,7 +21,7 @@ Section ILogic_Fun. Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index f5a22bd508..e91c004c77 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -26,7 +26,7 @@ Record morphism T T' `{e : type T} `{e' : type T'} := mkMorph { morph :> T -> T'; morph_resp : setoid_resp morph}. -Implicit Arguments mkMorph [T T' e e0 e' e1]. +Arguments mkMorph [T T' e0 e e1 e']. Infix "-s>" := morphism (at level 45, right associativity). Section Morphisms. Context {S T U V} `{eS : type S} `{eT : type T} `{eU : type U} `{eV : type V}. @@ -334,8 +334,8 @@ Section ILogic_Fun. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. -Implicit Arguments mkILFunFrm [T Frm ILOps]. +Arguments ILFunFrm _ {e} _ {ILOps}. +Arguments mkILFunFrm [T] _ [Frm ILOps]. Program Definition ILFun_eq {T R} {ILOps: ILogicOps R} {ILogic: ILogic R} (P : T -> R) : @ILFunFrm T _ R ILOps := diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 09f1149c20..13d62b8ff6 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -16,7 +16,7 @@ Section machine. | Inj : forall G, Prop -> propX G | ExistsX : forall G A, propX (A :: G) -> propX G. - Implicit Arguments Inj [G]. + Arguments Inj [G]. Definition PropX := propX nil. Fixpoint last (G : list Type) : Type. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index 8d7dfbd49b..bc9380f90d 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -23,7 +23,7 @@ Section ILogic_Fun. Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. End ILogic_Fun. -Implicit Arguments ILFunFrm [[ILOps] [e]]. +Arguments ILFunFrm _ {e} _ {ILOps}. Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; ltrue := True; land P Q := P /\ Q; diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v index c5bf3289bb..da4e53aab0 100644 --- a/test-suite/bugs/closed/4865.v +++ b/test-suite/bugs/closed/4865.v @@ -48,5 +48,5 @@ Fail Check g 0 0 1. (* 2nd 0 in bool *) Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. Notation "0" := true. -Arguments Scope lam [nat_scope nat_scope]. +Arguments lam _%nat_scope _%nat_scope : extra scopes. Check (lam 1 0). diff --git a/test-suite/bugs/closed/6631.v b/test-suite/bugs/closed/6631.v new file mode 100644 index 0000000000..100dc13fc8 --- /dev/null +++ b/test-suite/bugs/closed/6631.v @@ -0,0 +1,7 @@ +Require Import Coq.derive.Derive. + +Derive f SuchThat (f = 1 + 1) As feq. +Proof. + transitivity 2; [refine (eq_refl 2)|]. + transitivity 2. + 2:abstract exact (eq_refl 2). diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v new file mode 100644 index 0000000000..d90de8b932 --- /dev/null +++ b/test-suite/bugs/closed/7092.v @@ -0,0 +1,70 @@ +(* Examples matching fix/cofix in Ltac pattern-matching *) + +Goal True. +lazymatch (eval cbv delta [Nat.add] in Nat.add) with +| (fix F (n : nat) (v : ?A) {struct n} : @?P n v + := match n with + | O => @?O_case v + | S n' => @?S_case n' v F + end) + => + unify A nat; + unify P (fun _ _ : nat => nat); + unify O_case (fun v : nat => v); + unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat) + => S (add p m)) + end. +Abort. + +Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end +with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end. + +Goal True. + +lazymatch (eval cbv delta [f] in f) with +| fix myf (l : ?L) (n : ?N) {struct n} : nat := + match n as _ with + | 0 => ?Z + | S n0 => @?S myf myg n0 l + end + with myg (n' : ?N') (l' : ?L') {struct n'} : nat := + match n' as _ with + | 0 => ?Z' + | S n0' => @?S' myf myg n0' l' + end + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify Z 0; + unify Z' 1; + unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l)); + unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n) +end. + +Abort. + +CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2. + +CoFixpoint f' n l := C1 n (g' (cons n l) n n) +with g' l n p := C2 true (f' (S n) l). + +Goal True. + +lazymatch (eval cbv delta [f'] in f') with +| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l + with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l' + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify N'' nat; + unify T S1; + unify T' S2; + unify X (fun n g l => C1 n (g (cons n l) n n)); + unify X' (fun n f (l : list nat) => C2 true (f (S n) l)) +end. + +Abort. diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 6cca5c9fba..5294adefd3 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set. Inductive Catch (from to : nat) : Type := MkCatch : forall (p : Patch from to), Catch from to. -Implicit Arguments MkCatch [from to]. +Arguments MkCatch [from to]. Inductive CatchCommute5 : forall {from mid1 mid2 to : nat}, diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e333a..c09649de73 100644 --- a/test-suite/bugs/opened/3295.v +++ b/test-suite/bugs/opened/3295.v @@ -5,7 +5,7 @@ Class lops := lmk_ops { weq: relation car }. -Implicit Arguments car []. +Arguments car : clear implicits. Coercion car: lops >-> Sortclass. @@ -23,7 +23,7 @@ Class ops := mk_ops { dot: forall n m p, mor n m -> mor m p -> mor n p }. Coercion mor: ops >-> Funclass. -Implicit Arguments ob []. +Arguments ob : clear implicits. Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). Proof. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 08f489d751..a76fa19d3c 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Implicit Arguments ADMIT [p]. +Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index aa6b0a9a43..43c83e412a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected TO_SED_IN_BOTH=( -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index a148ebe8e6..0ef4b417a5 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ -Implicit Arguments eq [A]. +Arguments eq [A]. Fail Check (bool = true). diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 8ba8525c66..be33104918 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -1,8 +1,8 @@ Set Implicit Arguments. Unset Strict Implicit. -Implicit Arguments fst. -Implicit Arguments snd. +Arguments fst : default implicits. +Arguments snd : default implicits. Module Type PO. Parameter T : Set. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 7214287a6a..ece1b47b4f 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,7 +1,7 @@ Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. -Implicit Arguments ifte. +Arguments ifte : default implicits. Lemma Reflexivity_provable : forall (A : Set) (a : A) (s : {a = a} + {a <> a}), diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index 8700a6c4e2..6d9117c05c 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -2,8 +2,7 @@ Definition f (A:Type) (a:A) := a. -Local Arguments Scope f [type_scope type_scope]. -Local Implicit Arguments f [A]. +Local Arguments f [A]%type_scope _%type_scope. (* Used in ImportedCoercion.v to test the locality flag *) diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index b4efa7edca..d0aa5c8578 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -28,8 +28,8 @@ Class interp_pair (abs : Type) := { repr : term; link: abs = interp repr }. -Implicit Arguments repr [[interp_pair]]. -Implicit Arguments link [[interp_pair]]. +Arguments repr _ {interp_pair}. +Arguments link _ {interp_pair}. Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)). simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 921433cadd..9a19b595ef 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). -Implicit Arguments vector []. +Arguments vector A : clear implicits. Require Import Coq.Program.Program. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 5b1482fd58..f07c0191f1 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 45c71615fc..ca8da39482 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Implicit Arguments NL [I]. +Arguments NL [I]. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 8419404925..29350d620e 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -991,10 +991,10 @@ Proof. Qed. -Implicit Arguments Vector.cons [A n]. -Implicit Arguments Vector.nil [A]. -Implicit Arguments Vector.hd [A n]. -Implicit Arguments Vector.tl [A n]. +Arguments Vector.cons [A] _ [n]. +Arguments Vector.nil [A]. +Arguments Vector.hd [A n]. +Arguments Vector.tl [A n]. Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. @@ -1064,7 +1064,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} | S n', Vector.cons _ v' => vector_nth A n' _ v' end. -Implicit Arguments vector_nth [A p]. +Arguments vector_nth [A] _ [p]. Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, @@ -1159,7 +1159,7 @@ infiniteproof map_iterate'. Qed. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 6f27c1d369..18ebcd6384 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -5,7 +5,7 @@ Require Import Program. Require Import List. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. -Implicit Arguments vector []. +Arguments vector : clear implicits. Coercion vec_list : vector >-> list. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index ca37467166..2da630633d 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -11,7 +11,7 @@ Check (A.opp 3). Record B := { f :> Z -> Z }. Variable a:B. -Arguments Scope a [Z_scope]. +Arguments a _%Z_scope : extra scopes. Check a 0. (* Check that casts activate scopes if ever possible *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index cd6eac35cf..400479ae85 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Implicit Arguments unit [[m] [m0] [α]]. -Implicit Arguments Monad []. +Arguments unit {m m0 α}. +Arguments Monad : clear implicits. Notation "'return' t" := (unit t). (* Test correct handling of existentials and defined fields. *) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 02e043bc36..b287b5facf 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -39,7 +39,7 @@ Qed. (* Check apply/eapply distinction in presence of open terms *) Parameter h : forall x y z : nat, x = z -> x = y. -Implicit Arguments h [[x] [y]]. +Arguments h {x y}. Goal 1 = 0 -> True. intro H. apply h in H || exact I. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f5bb884d27..55ae54ca04 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -42,7 +42,7 @@ Inductive ctx : Type := Bind Scope context_scope with ctx. Delimit Scope context_scope with ctx. -Arguments Scope snoc [context_scope]. +Arguments snoc _%context_scope. Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 627794832d..5b13f35d57 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c }. -Implicit Arguments mkTri [R S T]. +Arguments mkTri [R S T]. Definition tri_iffT : tri iffT iffT iffT := (mkTri (fun X0 X1 X2 E01 E02 => diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index a0981311b1..23853890d8 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y. Definition eq2 := fun (A:Type) (x y:A) => x=y. Definition eq3 := fun (A:Type) (x y:A) => x=y. -Implicit Arguments op' []. -Global Implicit Arguments op'' []. +Arguments op' : clear implicits. +Global Arguments op'' : clear implicits. -Implicit Arguments eq2 []. -Global Implicit Arguments eq3 []. +Arguments eq2 : clear implicits. +Global Arguments eq3 : clear implicits. Check (op 0 0). Check (op' nat 0 0). @@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} := (* Check multiple implicit arguments signatures *) -Implicit Arguments eq_refl [[A] [x]] [[A]]. +Arguments eq_refl {A x}, {A}. Check eq_refl : 0 = 0. (* Check that notations preserve implicit (since 8.3) *) Parameter p : forall A, A -> forall n, n = 0 -> True. -Implicit Arguments p [A n]. +Arguments p [A] _ [n]. Notation Q := (p 0). Check Q eq_refl. diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el index 662762b08c..7c59fb6ae8 100644 --- a/tools/gallina-syntax.el +++ b/tools/gallina-syntax.el @@ -432,7 +432,6 @@ ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") ("Cd" nil "Cd #." nil "Cd") diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9ff4e33020..5dcc170b10 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2025,7 +2025,6 @@ let interp ?proof ~atts ~st c = | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> vernac_notation ~atts c infpl sc @@ -2099,8 +2098,6 @@ let interp ?proof ~atts ~st c = vernac_hints ~atts dbnames hints | VernacSyntacticDefinition (id,c,b) -> vernac_syntactic_definition ~atts id c b - | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl @@ -2168,7 +2165,7 @@ let check_vernac_supports_locality c l = | VernacDeclareMLModule _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ - | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ |