diff options
| -rw-r--r-- | .github/ISSUE_TEMPLATE.md (renamed from ISSUE_TEMPLATE.md) | 0 | ||||
| -rw-r--r-- | README.doc | 18 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 92 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 3 | ||||
| -rw-r--r-- | test-suite/Makefile | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/6129.v | 9 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh | 2 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5648.html.out | 18 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5648.tex.out | 12 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.html.out | 2 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.tex.out | 12 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.html.out | 6 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.tex.out | 12 | ||||
| -rw-r--r-- | vernac/class.ml | 64 |
17 files changed, 136 insertions, 128 deletions
diff --git a/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md index c9cb516cd..c9cb516cd 100644 --- a/ISSUE_TEMPLATE.md +++ b/.github/ISSUE_TEMPLATE.md diff --git a/README.doc b/README.doc deleted file mode 100644 index 4e72c894b..000000000 --- a/README.doc +++ /dev/null @@ -1,18 +0,0 @@ - The Coq documentation - ===================== - -The Coq documentation includes: - -- a reference manual; -- a generic tutorial on Coq; -- a tutorial on recursive types; -- a document presenting the Coq standard library; -- a list of questions/answers in the FAQ style - -All these documents are available online from the Coq official site -(http://coq.inria.fr), either as PS/PDF files or as HTML documents. - -The sources of the documentation are available along with the sources -of the Coq proof assistant. It is released under the Open Publication -License (see file doc/LICENSE in the sources of Coq) - diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 7e9373b29..7d3d811cc 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -54,9 +54,10 @@ Debugging from Caml debugger of each of error* functions or anomaly* functions in lib/util.ml - If "source db" fails, do a "make printers" and try again (it should build top_printers.cmo and the core cma files). - - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on - startup when run from the debugger. If this happens, unset the variable, - re-start Emacs, and run the debugger again. + - If you build Coq with an OCaml version earlier than 4.06, and have the + OCAMLRUNPARAM environment variable set, Coq may hang on startup when run + from the debugger. If this happens, unset the variable, re-start Emacs, and + run the debugger again. Global gprof-based profiling ============================ diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index ed41e3216..8f846f2f5 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -134,6 +134,7 @@ The optional file {\tt CoqMakefile.local} is included by the generated file compiler, like {\tt -bin-annot} or {\tt -w...}. \item[COQC, COQDEP, COQDOC] can be set in order to use alternative binaries (e.g. wrappers) + \item[COQ\_SRC\_SUBDIRS] can be extended by including other paths in which {\tt *.cm*} files are searched. For example {\tt COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq} lets you build a plugin containing OCaml code that depends on the OCaml code of {\tt Unicoq}. \end{description} \item[Rule extension] The following makefile rules can be extended. For example diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b0510dc7c..bf998933e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -309,11 +309,11 @@ let unfold_projection infos p c = else None (* Conversion between [lft1]term1 and [lft2]term2 *) -let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv +let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = + eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) -and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = +and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) let whd = whd_stack (infos_with_reds infos betaiotazeta) in @@ -338,13 +338,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then - let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect env l2r infos el1 el2 + let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in + convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) (Array.map (mk_clos env2) args2) cuniv else raise NotConvertible @@ -352,14 +352,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> if Int.equal (reloc_rel n el1) (reloc_rel m el2) - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try let cuniv = conv_table_key infos fl1 fl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in @@ -379,7 +379,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in - eqappr env cv_pb l2r infos app1 app2 cuniv) + eqappr cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -387,42 +387,42 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then - let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 u1 + let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 u1 else (* Two projections in WHNF: unfold *) raise NotConvertible) | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -434,15 +434,15 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in - let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv + let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in + ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) - let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv + let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in + ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> @@ -452,7 +452,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in - eqappr env CONV l2r infos + eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> let () = match v2 with @@ -461,34 +461,34 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in - eqappr env CONV l2r infos + eqappr CONV l2r infos (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -497,9 +497,9 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in let cuniv = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> @@ -508,16 +508,16 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in let cuniv = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> @@ -527,7 +527,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -535,14 +535,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> @@ -553,11 +553,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> @@ -568,11 +568,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) @@ -583,13 +583,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* In all other cases, terms are not convertible *) | _ -> raise NotConvertible -and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv = +and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv) + (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv -and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = +and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in let lv2 = Array.length v2 in if Int.equal lv1 lv2 @@ -597,7 +597,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let rec fold n cuniv = if n >= lv1 then cuniv else - let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in + let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in fold (n+1) cuniv in fold 0 cuniv else raise NotConvertible @@ -605,7 +605,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in - ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f708307c3..28abb7f57 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -58,7 +58,6 @@ let preamble mod_name comment used_modules usf = else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ str "import qualified GHC.Base" ++ fnl () ++ - str "import qualified GHC.Prim" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "import qualified IOExts" ++ fnl () ++ @@ -78,7 +77,7 @@ let preamble mod_name comment used_modules usf = (if not usf.tunknown then mt () else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ - str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "type Any = GHC.Base.Any" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "type Any = ()" ++ fnl () ++ diff --git a/test-suite/Makefile b/test-suite/Makefile index 61e75fa5d..7a204bfd8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -549,8 +549,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR $(coqc) -R coqdoc Coqdoc $* 2>&1; \ cd coqdoc; \ f=`basename $*`; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ if [ $$R = 0 -a $$S = 0 ]; then \ diff --git a/test-suite/bugs/closed/6129.v b/test-suite/bugs/closed/6129.v new file mode 100644 index 000000000..e4a2a2ba9 --- /dev/null +++ b/test-suite/bugs/closed/6129.v @@ -0,0 +1,9 @@ +(* Make definition of coercions compatible with local definitions. *) + +Record foo (x : Type) (y:=1) := { foo_nat :> nat }. +Record foo2 (x : Type) (y:=1) (z t: Type) := { foo_nat2 :> nat }. +Record foo3 (y:=1) (z t: Type) := { foo_nat3 :> nat }. + +Check fun x : foo nat => x + 1. +Check fun x : foo2 nat nat nat => x + 1. +Check fun x : foo3 nat nat => x + 1. diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 88606cd47..378573957 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -2,8 +2,6 @@ set -e -git clean -dfx - cat > _CoqProject <<EOT -I src/ diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 939ef9c7b..1b57a356b 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -2,8 +2,6 @@ set -e -git clean -dfx - cat > _CoqProject <<EOT -bypass-API -I src/ diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 06789c1c1..5c5a2dc29 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.bug5648</title> </head> @@ -31,14 +31,14 @@ <br/> <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> => 0<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> => 1<br/> - | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> => 2<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> => 3<br/> - | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> => 4<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> => 5<br/> - | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> => 6<br/> - | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> => 7<br/> + | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> ⇒ 0<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> ⇒ 1<br/> + | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> ⇒ 2<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> ⇒ 3<br/> + | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> ⇒ 4<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> ⇒ 5<br/> + | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> ⇒ 6<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> ⇒ 7<br/> <span class="id" title="keyword">end</span>.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out index b0b732eff..82f7da230 100644 --- a/test-suite/coqdoc/bug5648.tex.out +++ b/test-suite/coqdoc/bug5648.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 0e05660d6..b96fc6281 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.bug5700</title> </head> diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 33990cb89..1a1af5dfd 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index e2928f78d..70cbe5065 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Coqdoc.links</title> </head> @@ -57,7 +57,7 @@ Various checks for coqdoc <span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">forall</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> <br/> <span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> @@ -74,7 +74,7 @@ Various checks for coqdoc <span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> <span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index de3182d1a..7d93189ae 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/vernac/class.ml b/vernac/class.ml index f26599973..44f20a088 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -84,16 +84,9 @@ let check_target clt = function (* condition d'heritage uniforme *) -let uniform_cond sigma nargs lt = - let open EConstr in - let rec aux = function - | (0,[]) -> true - | (n,t::l) -> - let t = strip_outer_cast sigma t in - isRel sigma t && Int.equal (destRel sigma t) n && aux ((n-1),l) - | _ -> false - in - aux (nargs,lt) +let uniform_cond sigma ctx lt = + List.for_all2eq (EConstr.eq_constr sigma) + lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx) let class_of_global = function | ConstRef sp -> @@ -119,24 +112,29 @@ l'indice de la classe source dans la liste lp *) let get_source lp source = + let open Context.Rel.Declaration in match source with | None -> - let (cl1,u1,lv1) = - match lp with - | [] -> raise Not_found - | t1::_ -> find_class_type Evd.empty (EConstr.of_constr t1) - in - (cl1,u1,lv1,1) + (* Take the latest non let-in argument *) + let rec aux = function + | [] -> raise Not_found + | LocalDef _ :: lt -> aux lt + | LocalAssum (_,t1) :: lt -> + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + cl1,lt,lv1,1 + in aux lp | Some cl -> - let rec aux = function - | [] -> raise Not_found - | t1::lt -> - try - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in - if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1) - else raise Not_found - with Not_found -> aux lt - in aux (List.rev lp) + (* Take the first argument that matches *) + let rec aux acc = function + | [] -> raise Not_found + | LocalDef _ as decl :: lt -> aux (decl::acc) lt + | LocalAssum (_,t1) as decl :: lt -> + try + let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1 + else raise Not_found + with Not_found -> aux (decl::acc) lt + in aux [] (List.rev lp) let get_target t ind = if (ind > 1) then @@ -147,15 +145,6 @@ let get_target t ind = CL_PROJ p | x -> x - -let prods_of t = - let rec aux acc d = match Constr.kind d with - | Prod (_,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_,_) -> aux acc c - | _ -> (d,acc) - in - aux [] t - let strength_of_cl = function | CL_CONST kn -> `GLOBAL | CL_SECVAR id -> `LOCAL @@ -258,17 +247,18 @@ let add_new_coercion_core coef stre poly source target isid = check_source source; let t, _ = Global.type_of_global_in_context (Global.env ()) coef in if coercion_exists coef then raise (CoercionError AlreadyExists); - let tg,lp = prods_of t in + let lp,tg = decompose_prod_assum t in let llp = List.length lp in if Int.equal llp 0 then raise (CoercionError NotAFunction); - let (cls,us,lvs,ind) = + let (cls,ctx,lvs,ind) = try get_source lp source with Not_found -> raise (CoercionError (NoSource source)) in check_source (Some cls); - if not (uniform_cond Evd.empty (** FIXME *) (llp-ind) lvs) then + if not (uniform_cond Evd.empty (** FIXME - for when possibly called with unresolved evars in the future *) + ctx lvs) then warn_uniform_inheritance coef; let clt = try |