diff options
248 files changed, 895 insertions, 1379 deletions
diff --git a/API/API.mli b/API/API.mli index 8b0bef48c9..e3643076a3 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2763,6 +2763,7 @@ sig val pr_evar_info : Evd.evar_info -> Pp.t val print_constr : EConstr.constr -> Pp.t + val pr_sort_family : Sorts.family -> Pp.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -4046,7 +4047,6 @@ sig val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit - val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit @@ -4142,6 +4142,7 @@ sig val wit_global : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_ident : Names.Id.t Genarg.uniform_genarg_type val wit_integer : int Genarg.uniform_genarg_type + val wit_sort_family : (Sorts.family, unit, unit) Genarg.genarg_type val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type @@ -4773,6 +4774,7 @@ sig val global : reference Gram.entry val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry + val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry @@ -5333,7 +5335,7 @@ sig val lemInv_clause : Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Names.Id.t -> Constrexpr.constr_expr -> Misctypes.glob_sort -> bool -> (Names.Id.t -> unit Proofview.tactic) -> + Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) -> unit end @@ -13,6 +13,11 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. +Tools + +- In CoqIDE, the "Compile Buffer" command takes account of flags in + _CoqProject or other project file. + Changes from 8.6.1 to 8.7+beta ============================== @@ -7,7 +7,10 @@ The "Coq proof assistant" was jointly developed by associated to CNRS and university Paris Sud (since Sep. 1997), - Laboratoire d'Informatique de l'Ecole Polytechnique (LIX) associated to CNRS and Ecole Polytechnique (since Jan. 2003). -- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009). +- Laboratoire PPS associated to CNRS and University Paris Diderot + (Jan. 2009 - Dec. 2015). +- Institut de Recherche en Informatique Fondamentale (IRIF), + associated to CNRS and University Paris Diderot (since Jan. 2016). All files of the "Coq proof assistant" in directories or sub-directories of @@ -15,8 +18,8 @@ All files of the "Coq proof assistant" in directories or sub-directories of scripts states tactics test-suite theories tools toplevel are distributed under the terms of the GNU Lesser General Public License -Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010, -The Coq development team, CNRS, INRIA and Université Paris Sud. +Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2017, +The Coq development team, INRIA, CNRS, LIX, LRI, PPS. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -37,8 +40,8 @@ plugins/firstorder plugins/fourier developed by Loïc Pottier (INRIA-Lemme, 2001) plugins/funind - developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008), - Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) + developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now), + Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now) and Yves Bertot (INRIA-Marelle, 2005-2006) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) @@ -60,7 +63,7 @@ plugins/ssrmatching plugins/subtac developed by Matthieu Sozeau (LRI, 2005-2008) plugins/micromega - developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some + developed by Frédéric Besson (IRISA/INRIA, 2006-now), with some extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and interface to the csdp solver uses code from John Harrison (University of Cambridge, 1998) @@ -94,32 +97,41 @@ of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) Yves Bertot (INRIA, 2000-now) - Pierre Boutillier (INRIA-PPS, 2010-now) + Pierre Boutillier (INRIA-PPS, 2010-2015) Xavier Clerc (INRIA, 2012-2014) + Tej Chajed (MIT, 2016-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011) Cristina Cornes (INRIA, 1993-1996) Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996) + Pierre Courtieu (CNAM, 2006-now) David Delahaye (INRIA, 1997-2002) Maxime Dénès (INRIA, 2013-now) - Daniel de Rauglaudre (INRIA, 1996-1998) + Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016) Olivier Desmettre (INRIA, 2001-2003) Gilles Dowek (INRIA, 1991-1994) Amy Felty (INRIA, 1993) Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008) + Emilio Jesús Gallego Arias (MINES ParisTech 2015-now) + Gaetan Gilbert (INRIA-CoqHoTT 2016-now) Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) Stéphane Glondu (INRIA-PPS, 2007-2013) Benjamin Grégoire (INRIA, 2003-2011) + Jason Gross (MIT 2013-now) Hugo Herbelin (INRIA, 1996-now) Sébastien Hinderer (INRIA, 2014) Gérard Huet (INRIA, 1985-1997) + Matej Košík (INRIA, 2015-2017) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now) Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) + Gregory Malecha (Harvard University 2013-2015, + University of California, San Diego 2016) + Cyprien Mangin (INRIA-IRIF, 2015-now) Pascal Manoury (INRIA, 1993) - Micaela Mayero (INRIA, 1997-2002) Claude Marché (INRIA, 2003-2004 & LRI, 2004) + Micaela Mayero (INRIA, 1997-2002) Guillaume Melquiond (INRIA, 2009-now) Benjamin Monate (LRI, 2003) César Muñoz (INRIA, 1994-1995) @@ -129,7 +141,8 @@ of the Coq Proof assistant during the indicated time: Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-2006) - Pierre-Marie Pédrot (INRIA-PPS, 2011-now) + Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-CoqHoTT 2015-2016, + University of Ljubljana 2016-2017) Matthias Puech (INRIA-Bologna, 2008-2011) Yann Régis-Gianas (INRIA-PPS, 2009-now) Clément Renard (INRIA, 2001-2004) @@ -138,9 +151,15 @@ of the Coq Proof assistant during the indicated time: Vincent Siles (INRIA, 2007) Élie Soubiran (INRIA, 2007-2010) Matthieu Sozeau (INRIA, 2005-now) - Arnaud Spiwack (INRIA, 2006-now) + Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010, + INRIA, 2011-2014, MINES ParisTech 2014-2015, + Tweag/IO 2015-now) + Paul Steckler (MIT 2016-now) Enrico Tassi (INRIA, 2011-now) + Amin Timany (Katholieke Universiteit Leuven, 2017) Benjamin Werner (INRIA, 1989-1994) + Nickolai Zeldovich (MIT 2014-2016) + Théo Zimmermann (INRIA-IRIF, 2015-now) *************************************************************************** INRIA refers to: diff --git a/checker/univ.ml b/checker/univ.ml index 558315c2c1..4f31318132 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -29,107 +29,6 @@ open Util union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -module type Hashconsed = -sig - type t - val hash : t -> int - val eq : t -> t -> bool - val hcons : t -> t -end - -module HashedList (M : Hashconsed) : -sig - type t = private Nil | Cons of M.t * int * t - val nil : t - val cons : M.t -> t -> t -end = -struct - type t = Nil | Cons of M.t * int * t - module Self = - struct - type _t = t - type t = _t - type u = (M.t -> M.t) - let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 - | _ -> false - let hashcons hc = function - | Nil -> Nil - | Cons (x, h, l) -> Cons (hc x, h, l) - end - module Hcons = Hashcons.Make(Self) - let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons - (** No recursive call: the interface guarantees that all HLists from this - program are already hashconsed. If we get some external HList, we can - still reconstruct it by traversing it entirely. *) - let nil = Nil - let cons x l = - let h = M.hash x in - let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in - let h = Hashset.Combine.combine h hl in - hcons (Cons (x, h, l)) -end - -module HList = struct - - module type S = sig - type elt - type t = private Nil | Cons of elt * int * t - val hash : t -> int - val nil : t - val cons : elt -> t -> t - val tip : elt -> t - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val map : (elt -> elt) -> t -> t - val smartmap : (elt -> elt) -> t -> t - val exists : (elt -> bool) -> t -> bool - val for_all : (elt -> bool) -> t -> bool - val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val to_list : t -> elt list - end - - module Make (H : Hashconsed) : S with type elt = H.t = - struct - type elt = H.t - include HashedList(H) - - let hash = function Nil -> 0 | Cons (_, h, _) -> h - - let tip e = cons e nil - - let rec fold f l accu = match l with - | Nil -> accu - | Cons (x, _, l) -> fold f l (f x accu) - - let rec map f = function - | Nil -> nil - | Cons (x, _, l) -> cons (f x) (map f l) - - let smartmap = map - (** Apriori hashconsing ensures that the map is equal to its argument *) - - let rec exists f = function - | Nil -> false - | Cons (x, _, l) -> f x || exists f l - - let rec for_all f = function - | Nil -> true - | Cons (x, _, l) -> f x && for_all f l - - let rec for_all2 f l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2 - | _ -> false - - let rec to_list = function - | Nil -> [] - | Cons (x, _, l) -> x :: to_list l - - end -end - module RawLevel = struct open Names @@ -167,24 +66,6 @@ struct | _, Level _ -> 1 | Var n, Var m -> Int.compare n m - let hequal x y = - x == y || - match x, y with - | Prop, Prop -> true - | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' - | Var n, Var n' -> n == n' - | _ -> false - - let hcons = function - | Prop as x -> x - | Set as x -> x - | Level (n,d) as x -> - let d' = Names.DirPath.hcons d in - if d' == d then x else Level (n,d') - | Var n as x -> x - open Hashset.Combine let hash = function @@ -216,24 +97,7 @@ module Level = struct let data x = x.data - (** Hashcons on levels + their hash *) - - module Self = struct - type _t = t - type t = _t - type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data - let hash x = x.hash - let hashcons () x = - let data' = RawLevel.hcons x.data in - if x.data == data' then x else { x with data = data' } - end - - let hcons = - let module H = Hashcons.Make(Self) in - Hashcons.simple_hcons H.generate H.hcons () - - let make l = hcons { hash = RawLevel.hash l; data = l } + let make l = { hash = RawLevel.hash l; data = l } let set = make Set let prop = make Prop @@ -270,7 +134,7 @@ module Level = struct let pr u = str (to_string u) - let make m n = make (Level (n, Names.DirPath.hcons m)) + let make m n = make (Level (n, m)) end @@ -303,48 +167,12 @@ struct module Expr = struct type t = Level.t * int - type _t = t - (* Hashing of expressions *) - module ExprHash = - struct - type t = _t - type u = Level.t -> Level.t - let hashcons hdir (b,n as x) = - let b' = hdir b in - if b' == b then x else (b',n) - let eq l1 l2 = - l1 == l2 || - match l1,l2 with - | (b,n), (b',n') -> b == b' && n == n' - - let hash (x, n) = n + Level.hash x - - end - - module HExpr = - struct - - module H = Hashcons.Make(ExprHash) - - type t = ExprHash.t - - let hcons = - Hashcons.simple_hcons H.generate H.hcons Level.hcons - let hash = ExprHash.hash - let eq x y = x == y || - (let (u,n) = x and (v,n') = y in - Int.equal n n' && Level.equal u v) - - end - - let hcons = HExpr.hcons - - let make l = hcons (l, 0) + let make l = (l, 0) - let prop = make Level.prop - let set = make Level.set - let type1 = hcons (Level.set, 1) + let prop = (Level.prop, 0) + let set = (Level.set, 0) + let type1 = (Level.set, 1) let is_prop = function | (l,0) -> Level.is_prop l @@ -363,13 +191,13 @@ struct let successor (u,n) = if Level.is_prop u then type1 - else hcons (u, n + 1) + else (u, n + 1) let addn k (u,n as x) = if k = 0 then x else if Level.is_prop u then - hcons (Level.set,n+k) - else hcons (u,n+k) + (Level.set,n+k) + else (u,n+k) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in @@ -394,31 +222,29 @@ struct let v' = f v in if v' == v then x else if Level.is_prop v' && n != 0 then - hcons (Level.set, n) - else hcons (v', n) + (Level.set, n) + else (v', n) end - - module Huniv = HList.Make(Expr.HExpr) - type t = Huniv.t - open Huniv - - let equal x y = x == y || - (Huniv.hash x == Huniv.hash y && - Huniv.for_all2 Expr.equal x y) - let make l = Huniv.tip (Expr.make l) - let tip x = Huniv.tip x - + type t = Expr.t list + + let tip u = [u] + let cons u v = u :: v + + let equal x y = x == y || List.equal Expr.equal x y + + let make l = tip (Expr.make l) + let pr l = match l with - | Cons (u, _, Nil) -> Expr.pr u + | [u] -> Expr.pr u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ + (prlist_with_sep pr_comma Expr.pr l) ++ str ")" let level l = match l with - | Cons (l, _, Nil) -> Expr.level l + | [l] -> Expr.level l | _ -> None (* The lower predicative level of the hierarchy that contains (impredicative) @@ -438,16 +264,16 @@ struct (* Returns the formal universe that lies juste above the universe variable u. Used to type the sort u. *) let super l = - Huniv.map (fun x -> Expr.successor x) l + List.map (fun x -> Expr.successor x) l let addn n l = - Huniv.map (fun x -> Expr.addn n x) l + List.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons (h1, _, t1), Cons (h2, _, t2) -> + | [], _ -> l2 + | _, [] -> l1 + | h1 :: t1, h2 :: t2 -> (match Expr.super h1 h2 with | Inl true (* h1 < h2 *) -> merge_univs t1 l2 | Inl false -> merge_univs l1 t2 @@ -459,28 +285,28 @@ struct let sort u = let rec aux a l = match l with - | Cons (b, _, l') -> + | b :: l' -> (match Expr.super a b with | Inl false -> aux a l' | Inl true -> l | Inr c -> if c <= 0 then cons a l else cons b (aux a l')) - | Nil -> cons a l + | [] -> cons a l in - fold (fun a acc -> aux a acc) u nil + List.fold_right (fun a acc -> aux a acc) u [] (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y - let empty = nil + let empty = [] - let exists = Huniv.exists + let exists = List.exists - let for_all = Huniv.for_all + let for_all = List.for_all - let smartmap = Huniv.smartmap + let smartmap = List.smartmap end @@ -768,9 +594,9 @@ let check_equal_expr g x y = let check_eq_univs g l1 l2 = let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in - Huniv.for_all (fun x1 -> exists x1 l2) l1 - && Huniv.for_all (fun x2 -> exists x2 l1) l2 + let exists x1 l = List.exists (fun x2 -> f x1 x2) l in + List.for_all (fun x1 -> exists x1 l2) l1 + && List.for_all (fun x2 -> exists x2 l1) l2 let check_eq g u v = Universe.equal u v || check_eq_univs g u v @@ -784,11 +610,11 @@ let check_smaller_expr g (u,n) (v,m) = | _ -> false let exists_bigger g ul l = - Huniv.exists (fun ul' -> + Universe.exists (fun ul' -> check_smaller_expr g ul ul') l let real_check_leq g u v = - Huniv.for_all (fun ul -> exists_bigger g ul v) u + Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = Universe.equal u v || @@ -1026,8 +852,8 @@ let check_univ_leq u v = let enforce_leq u v c = match v with - | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) -> - Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c + | [v] -> + List.fold_right (fun u -> constraint_add_leq u v) u c | _ -> anomaly (Pp.str"A universe bound can only be a variable.") let enforce_leq u v c = @@ -1080,63 +906,18 @@ end = struct type t = Level.t array - let empty : t = [||] - - module HInstancestruct = - struct - type _t = t - type t = _t - type u = Level.t -> Level.t - - let hashcons huniv a = - let len = Array.length a in - if Int.equal len 0 then empty - else begin - for i = 0 to len - 1 do - let x = Array.unsafe_get a i in - let x' = huniv x in - if x == x' then () - else Array.unsafe_set a i x' - done; - a - end - - let eq t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) - in aux 0) - - let hash a = - let accu = ref 0 in - for i = 0 to Array.length a - 1 do - let l = Array.unsafe_get a i in - let h = Level.hash l in - accu := Hashset.Combine.combine !accu h; - done; - (* [h] must be positive. *) - let h = !accu land 0x3FFFFFFF in - h - - end - - module HInstance = Hashcons.Make(HInstancestruct) - - let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons - - let empty = hcons [||] + let empty = [||] let is_empty x = Int.equal (Array.length x) 0 let subst_fn fn t = let t' = CArray.smartmap fn t in - if t' == t then t else hcons t' + if t' == t then t else t' let subst s t = let t' = CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t - in if t' == t then t else hcons t' + in if t' == t then t else t' let pr = prvect_with_sep spc Level.pr @@ -1296,7 +1077,7 @@ let subst_univs_expr_opt fn (l,n) = let subst_univs_universe fn ul = let subst, nosubst = - Universe.Huniv.fold (fun u (subst,nosubst) -> + List.fold_right (fun u (subst,nosubst) -> try let a' = subst_univs_expr_opt fn u in (a' :: subst, nosubst) with Not_found -> (subst, u :: nosubst)) @@ -1307,7 +1088,7 @@ let subst_univs_universe fn ul = let substs = List.fold_left Universe.merge_univs Universe.empty subst in - List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) + List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst let merge_context strict ctx g = diff --git a/checker/univ.mli b/checker/univ.mli index 0a21019b1b..0eadc6801f 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -164,7 +164,6 @@ sig val is_empty : t -> bool val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) diff --git a/checker/values.ml b/checker/values.ml index afde84854c..86634fbd80 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -99,7 +99,7 @@ let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;Int|] -let rec v_univ = Sum ("universe", 1, [| [|v_expr; Int; v_univ|] |]) +let v_univ = List v_expr let v_cstrs = Annot diff --git a/dev/doc/changes.txt b/dev/doc/changes.md index 0f1a28028c..5ed74917aa 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.md @@ -1,141 +1,146 @@ -========================================= -= CHANGES BETWEEN COQ V8.7 AND COQ V8.8 = -========================================= +## Changes between Coq 8.7 and Coq 8.8 -* ML API * +### Plugin API + +Coq 8.8 offers a new module overlay containing a proposed plugin API +in `API/API.ml`; this overlay is enabled by adding the `-open API` +flag to the OCaml compiler; this happens automatically for +developments in the `plugin` folder and `coq_makefile`. + +However, `coq_makefile` can be instructed not to enable this flag by +passing `-bypass-API`. + +### ML API We removed the following functions: -- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context +- `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` instead. The returned term contains De Bruijn universe variables. If you don't depend on universes being instantiated, simply drop the context. -- Universes.unsafe_type_of_global: same as above with - Global.type_of_global_in_context + +- `Universes.unsafe_type_of_global`: same as above with + `Global.type_of_global_in_context` We changed the type of the following functions: -- Global.body_of_constant_body: now also returns the abstract universe context. +- `Global.body_of_constant_body`: now also returns the abstract universe context. The returned term contains De Bruijn universe variables. -- Global.body_of_constant: same as above. + +- `Global.body_of_constant`: same as above. We renamed the following datatypes: - Pp.std_ppcmds -> Pp.t +- `Pp.std_ppcmds` -> `Pp.t` -========================================= -= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = -========================================= +## Changes between Coq 8.6 and Coq 8.7 -* Ocaml * +### Ocaml -Coq is compiled with -safe-string enabled and requires plugins to do +Coq is compiled with `-safe-string` enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` -* Plugin API * +### ML API -Coq 8.7 offers a new module overlay containing a proposed plugin API -in `API/API.ml`; this overlay is enabled by adding the `-open API` -flag to the OCaml compiler; this happens automatically for -developments in the `plugin` folder and `coq_makefile`. - -However, `coq_makefile` can be instructed not to enable this flag by -passing `-bypass-API`. - -* ML API * - -Added two functions for declaring hooks to be executed in reduction +- Added two functions for declaring hooks to be executed in reduction functions when some given constants are traversed: - declare_reduction_effect: to declare a hook to be applied when some + * `declare_reduction_effect`: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv). - set_reduction_effect: to declare a constant on which a given effect + * `set_reduction_effect`: to declare a constant on which a given effect hook should be called. -We renamed the following functions: +- We renamed the following functions: + ``` Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr Printer.pr_var_list_decl -> Printer.pr_compacted_decl Printer.pr_var_decl -> Printer.pr_named_decl Nameops.lift_subscript -> Nameops.increment_subscript + ``` -We removed the following functions: +- We removed the following functions: - Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context - Namegen.to_avoid ... equivalent substitute is Names.Id.List.mem + * `Termops.compact_named_context_reverse`: practical substitute is `Termops.compact_named_context`. + * `Namegen.to_avoid`: equivalent substitute is `Names.Id.List.mem`. -We renamed the following modules: +- We renamed the following modules: - Context.ListNamed -> Context.Compacted + * `Context.ListNamed` -> `Context.Compacted` -The following type aliases where removed +- The following type aliases where removed - Context.section_context ... it was just an alias for "Context.Named.t" which is still available + * `Context.section_context`: it was just an alias for `Context.Named.t` which is still available. -The module Constrarg was merged into Stdarg. +- The module `Constrarg` was merged into `Stdarg`. -The following types have been moved and modified: +- The following types have been moved and modified: - local_binder -> local_binder_expr - glob_binder merged with glob_decl + * `local_binder` -> `local_binder_expr` + * `glob_binder` merged with `glob_decl` -The following constructors have been renamed: +- The following constructors have been renamed: + ``` LocalRawDef -> CLocalDef LocalRawAssum -> CLocalAssum LocalPattern -> CLocalPattern + ``` -In Constrexpr_ops: +- In `Constrexpr_ops`: - Deprecating abstract_constr_expr in favor of mkCLambdaN, and - prod_constr_expr in favor of mkCProdN. Note: the first ones were - interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second + Deprecating `abstract_constr_expr` in favor of `mkCLambdaN`, and + `prod_constr_expr` in favor of `mkCProdN`. Note: the first ones were + interpreting `(x y z:_)` as `(x:_) (y:_) (z:_)` while the second ones were preserving the original sharing of the type. -In Nameops: +- In `Nameops`: The API has been made more uniform. New combinators added in the - "Name" space name. Function "out_name" now fails with IsAnonymous - rather than with Failure "Nameops.out_name". + `Name` space name. Function `out_name` now fails with `IsAnonymous` + rather than with `Failure "Nameops.out_name"`. -Location handling and AST attributes: +- Location handling and AST attributes: - Location handling has been reworked. First, Loc.ghost has been + Location handling has been reworked. First, `Loc.ghost` has been removed in favor of an option type, all objects carrying an optional source code location have been switched to use `Loc.t option`. Storage of location information has been also refactored. The main - datatypes representing Coq AST (constrexpr, glob_expr) have been + datatypes representing Coq AST (`constrexpr`, `glob_expr`) have been switched to a generic "node with attributes" representation `'a CAst.ast`, which is a record of the form: -```ocaml -type 'a ast = private { - v : 'a; - loc : Loc.t option; - ... -} -``` + ```ocaml + type 'a ast = private { + v : 'a; + loc : Loc.t option; + ... + } + ``` consumers of AST nodes are recommended to use accessor-based pattern matching `{ v; loc }` to destruct `ast` object. Creation is done with `CAst.make ?loc obj`, where the attributes are optional. Some convenient combinators are provided in the module. A typical match: -``` -| CCase(loc, a1) -> CCase(loc, f a1) -``` + + ```ocaml + | CCase(loc, a1) -> CCase(loc, f a1) + ``` + is now done as: -``` -| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) -``` + ```ocaml + | { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) + + ``` or even better, if plan to preserve the attributes you can wrap your top-level function in `CAst.map` to have: -``` -| CCase(a1) -> CCase(f a1) -``` + ```ocaml + | CCase(a1) -> CCase(f a1) + ``` This scheme based on records enables easy extensibility of the AST node type without breaking compatibility. @@ -151,14 +156,14 @@ type 'a ast = private { implemented in the whole code base. Matching a located object hasn't changed, however, `Loc.tag ?loc obj` must be used to build one. -In GOption: +- In `GOption`: Support for non-synchronous options has been removed. Now all options are handled as a piece of normal document state, and thus passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. -In Coqlib / reference location: +- In `Coqlib` / reference location: We have removed from Coqlib functions returning `constr` from names. Now it is only possible to obtain references, that must be @@ -175,65 +180,67 @@ In Coqlib / reference location: `pf_constr_of_global` in tactics and `Evarutil.new_global` variants when constructing terms in ML (see univpoly.txt for more information). -** Tactic API ** +### Tactic API -- pf_constr_of_global now returns a tactic instead of taking a continuation. +- `pf_constr_of_global` now returns a tactic instead of taking a continuation. Thus it only generates one instance of the global reference, and it is the caller's responsibility to perform a focus on the goal. -- pf_global, construct_reference, global_reference, - global_reference_in_absolute_module now return a global_reference - instead of a constr. +- `pf_global`, `construct_reference`, `global_reference`, + `global_reference_in_absolute_module` now return a `global_reference` + instead of a `constr`. -- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase - was very specific. Use tclPROGRESS instead. +- The `tclWEAK_PROGRESS` and `tclNOTSAMEGOAL` tacticals were removed. Their usecase + was very specific. Use `tclPROGRESS` instead. - New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows to iterate a non-unit tactic on all goals and access their returned values. -- The unsafe flag of the Refine.refine function and its variants has been +- The unsafe flag of the `Refine.refine` function and its variants has been renamed and dualized into typecheck and has been made mandatory. -** Ltac API ** +### Ltac API Many Ltac specific API has been moved in its own ltac/ folder. Amongst other important things: -- Pcoq.Tactic -> Pltac -- Constrarg.wit_tactic -> Tacarg.wit_tactic -- Constrarg.wit_ltac -> Tacarg.wit_ltac -- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument +- `Pcoq.Tactic` -> `Pltac` +- `Constrarg.wit_tactic` -> `Tacarg.wit_tactic` +- `Constrarg.wit_ltac` -> `Tacarg.wit_ltac` +- API below `ltac/` that accepted a *`_tactic_expr` now accept a *`_generic_argument` instead -- Some printing functions were moved from Pptactic to Pputils -- A part of Tacexpr has been moved to Tactypes -- The TacFun tactic expression constructor now takes a `Name.t list` for the +- Some printing functions were moved from `Pptactic` to `Pputils` +- A part of `Tacexpr` has been moved to `Tactypes` +- The `TacFun` tactic expression constructor now takes a `Name.t list` for the variable list rather than an `Id.t option list`. The folder itself has been turned into a plugin. This does not change much, but because it is a packed plugin, it may wreak havoc for third-party plugins -depending on any module defined in the ltac/ directory. Namely, even if +depending on any module defined in the `ltac/` directory. Namely, even if everything looks OK at compile time, a plugin can fail to load at link time -because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +because it mistakenly looks for a module `Foo` instead of `Ltac_plugin.Foo`, with an error of the form: +``` Error: while loading myplugin.cmxs, no implementation available for Foo. +``` -In particular, most EXTEND macros will trigger this problem even if they +In particular, most `EXTEND` macros will trigger this problem even if they seemingly do not use any Ltac module, as their expansion do. -The solution is simple, and consists in adding a statement "open Ltac_plugin" +The solution is simple, and consists in adding a statement `open Ltac_plugin` in each file using a Ltac module, before such a module is actually called. An alternative solution would be to fully qualify Ltac modules, e.g. turning any -call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not -work for EXTEND macros though. +call to Tacinterp into `Ltac_plugin.Tacinterp`. Note that this solution does not +work for `EXTEND` macros though. -** Additional changes in tactic extensions ** +### Additional changes in tactic extensions -Entry "constr_with_bindings" has been renamed into -"open_constr_with_bindings". New entry "constr_with_bindings" now +Entry `constr_with_bindings` has been renamed into +`open_constr_with_bindings`. New entry `constr_with_bindings` now uses type classes and rejects terms with unresolved holes. -** Error handling ** +### Error handling - All error functions now take an optional parameter `?loc:Loc.t`. For functions that used to carry a suffix `_loc`, such suffix has been @@ -243,14 +250,14 @@ uses type classes and rejects terms with unresolved holes. - The header parameter to `user_err` has been made optional. -** Pretty printing ** +### Pretty printing Some functions have been removed, see pretty printing below for more details. -* Pretty Printing and XML protocol * +#### Pretty Printing and XML protocol -The type std_cmdpps has been reworked and made the canonical "Coq rich +The type `std_cmdpps` has been reworked and made the canonical "Coq rich document type". This allows for a more uniform handling of printing (specially in IDEs). The main consequences are: @@ -267,12 +274,13 @@ document type". This allows for a more uniform handling of printing - `Pp_control` has removed. The new module `Topfmt` implements console control for the toplevel. - - The impure tag system in Pp has been removed. This also does away + - The impure tag system in `Pp` has been removed. This also does away with the printer signatures and functors. Now printers tag unconditionally. - The following functions have been removed from `Pp`: + ```ocaml val stras : int * string -> std_ppcmds val tbrk : int * int -> std_ppcmds val tab : unit -> std_ppcmds @@ -294,8 +302,9 @@ document type". This allows for a more uniform handling of printing val msg_with : ... module Tag + ``` -** Stm API ** +### Stm API - We have streamlined the `Stm` API, now `add` and `query` take a `coq_parsable` instead a `string` so clients can have more control @@ -312,7 +321,7 @@ document type". This allows for a more uniform handling of printing - A few unused hooks were removed due to cleanups, no clients known. -** Toplevel and Vernacular API ** +### Toplevel and Vernacular API - The components related to vernacular interpretation have been moved to their own folder `vernac/` whereas toplevel now contains the @@ -321,39 +330,41 @@ document type". This allows for a more uniform handling of printing - Coq's toplevel has been ported to directly use the common `Stm` API. The signature of a few functions has changed as a result. -** XML Protocol ** +### XML Protocol - The legacy `Interp` call has been turned into a noop. - The `query` call has been modified, now it carries a mandatory - "route_id" integer parameter, that associated the result of such + `route_id` integer parameter, that associated the result of such query with its generated feedback. -========================================= -= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = -========================================= +## Changes between Coq 8.5 and Coq 8.6 -** Parsing ** +### Parsing -Pcoq.parsable now takes an extra optional filename argument so as to +`Pcoq.parsable` now takes an extra optional filename argument so as to bind locations to a file name when relevant. -** Files ** +### Files To avoid clashes with OCaml's compiler libs, the following files were renamed: + +``` kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} lib/errors.ml{,i} -> lib/cErrors.ml{,i} toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} +``` -All IDE-specific files, including the XML protocol have been moved to ide/ +All IDE-specific files, including the XML protocol have been moved to `ide/` -** Reduction functions ** +### Reduction functions -In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, -fCOFIX. +In `closure.ml`, we introduced the more precise reduction flags `fMATCH`, `fFIX`, +`fCOFIX`. We renamed the following functions: +``` Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta @@ -380,9 +391,11 @@ Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all +``` And removed the following ones: +``` Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state @@ -392,15 +405,16 @@ Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta +``` -In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and -FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. +In `intf/genredexpr.mli`, `fIota` was replaced by `FMatch`, `FFix` and +`FCofix`. Similarly, `rIota` was replaced by `rMatch`, `rFix` and `rCofix`. -** Notation_ops ** +### Notation_ops -Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. +Use `Glob_ops.glob_constr_eq` instead of `Notation_ops.eq_glob_constr`. -** Logging and Pretty Printing: ** +### Logging and Pretty Printing * Printing functions have been removed from `Pp.mli`, which is now a purely pretty-printing interface. Functions affected are: @@ -429,7 +443,7 @@ val message : string -> unit * Feedback related functions and definitions have been moved to the `Feedback` module. `message_level` has been renamed to - level. Functions moved from Pp to Feedback are: + level. Functions moved from `Pp` to `Feedback` are: ```` ocaml val set_logger : logger -> unit @@ -474,12 +488,13 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit val get_id_for_feedback : unit -> edit_or_state_id * route_id ```` -** Kernel API changes ** +### Kernel API changes -- The interface of the Context module was changed. +- The interface of the `Context` module was changed. Related types and functions were put in separate submodules. The mapping from old identifiers to new identifiers is the following: + ``` Context.named_declaration ---> Context.Named.Declaration.t Context.named_list_declaration ---> Context.NamedList.Declaration.t Context.rel_declaration ---> Context.Rel.Declaration.t @@ -521,123 +536,142 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Context.rel_context_length ---> Context.Rel.length Context.rel_context_nhyps ---> Context.Rel.nhyps Context.rel_context_tags ---> Context.Rel.to_tags + ``` - Originally, rel-context was represented as: - Context.rel_context = Names.Name.t * Constr.t option * Constr.t + ```ocaml + type Context.rel_context = Names.Name.t * Constr.t option * Constr.t + ``` Now it is represented as: - Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t - + ```ocaml + type Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t + | LocalDef of Names.Name.t * Constr.t * Constr.t + ``` + - Originally, named-context was represented as: - Context.named_context = Names.Id.t * Constr.t option * Constr.t + ```ocaml + type Context.named_context = Names.Id.t * Constr.t option * Constr.t + ``` Now it is represented as: - Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t + ```ocaml + type Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t + | LocalDef of Names.Id.t * Constr.t * Constr.t + ``` -- The various EXTEND macros do not handle specially the Coq-defined entries +- The various `EXTEND` macros do not handle specially the Coq-defined entries anymore. Instead, they just output a name that have to exist in the scope - of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for - variables "$name" of type Gram.entry, while the parsing rules of - (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will - look for variables "wit_$name" of type Genarg.genarg_type. The small DSL + of the ML code. The parsing rules (`VERNAC`) `ARGUMENT EXTEND` will look for + variables `$name` of type `Gram.entry`, while the parsing rules of + (`VERNAC COMMAND` | `TACTIC`) `EXTEND`, as well as the various `TYPED AS` clauses will + look for variables `wit_$name` of type `Genarg.genarg_type`. The small DSL for constructing compound entries still works over this scheme. Note that in - the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound + the case of (`VERNAC`) `ARGUMENT EXTEND`, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. - For example, to get "wit_constr" you must "open Constrarg" at the top of the file. + For example, to get `wit_constr` you must `open Constrarg` at the top of the file. -- Evarutil was split in two parts. The new Evardefine file exposes functions -define_evar_* mostly used internally in the unification engine. +- `Evarutil` was split in two parts. The new `Evardefine` file exposes functions + `define_evar_`* mostly used internally in the unification engine. -- The Refine module was move out of Proofview. +- The `Refine` module was moved out of `Proofview`. + ``` Proofview.Refine.* ---> Refine.* + ``` -- A statically monotonous evarmap type was introduced in Sigma. Not all the API +- A statically monotonic evarmap type was introduced in `Sigma`. Not all the API has been converted, so that the user may want to use compatibility functions - Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when + `Sigma.to_evar_map` and `Sigma.Unsafe.of_evar_map` or `Sigma.Unsafe.of_pair` when needed. Code can be straightforwardly adapted in the following way: + ```ocaml let (sigma, x1) = ... in ... let (sigma, xn) = ... in (sigma, ans) + ``` should be turned into: + ```ocaml open Sigma.Notations let Sigma (x1, sigma, p1) = ... in ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + ``` Examples of `Sigma.Unsafe.of_evar_map` include: + ``` Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty + ``` -- The Proofview.Goal.*enter family of functions now takes a polymorphic +- The `Proofview.Goal.`*`enter` family of functions now takes a polymorphic continuation given as a record as an argument. + ```ocaml Proofview.Goal.enter begin fun gl -> ... end + ``` should be turned into + ```ocaml open Proofview.Notations Proofview.Goal.enter { enter = begin fun gl -> ... end } + ``` - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` - `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` - `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` - (`Global.named_context` ---> `Global.named_context_val`) - (`Context.Named.lookup` ---> `Environ.lookup_named_val`) +- `Global.named_context` ---> `Global.named_context_val` +- `Context.Named.lookup` ---> `Environ.lookup_named_val` -** Search API ** +### Search API The main search functions now take a function iterating over the results. This allows for clients to use streaming or more economic printing. -========================================= -= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = -========================================= +## Changes between Coq 8.4 and Coq 8.5 -** Refactoring : more mli interfaces and simpler grammar.cma ** +### Refactoring : more mli interfaces and simpler grammar.cma - A new directory intf/ now contains mli-only interfaces : - Constrexpr : definition of constr_expr, was in Topconstr - Decl_kinds : now contains binding_kind = Explicit | Implicit - Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind - Extend : was parsing/extend.mli - Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag - Glob_term : definition of glob_constr - Locus : definition of occurrences and stuff about clauses - Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ... - Notation_term : contains notation_constr, was Topconstr.aconstr - Pattern : contains constr_pattern - Tacexpr : was tactics/tacexpr.ml - Vernacexpr : was toplevel/vernacexpr.ml + * `Constrexpr` : definition of `constr_expr`, was in `Topconstr` + * `Decl_kinds` : now contains `binding_kind = Explicit | Implicit` + * `Evar_kinds` : type `Evar_kinds.t` was previously `Evd.hole_kind` + * `Extend` : was `parsing/extend.mli` + * `Genredexpr` : regroup `Glob_term.red_expr_gen` and `Tacexpr.glob_red_flag` + * `Glob_term` : definition of `glob_constr` + * `Locus` : definition of occurrences and stuff about clauses + * `Misctypes` : `intro_pattern_expr`, `glob_sort`, `cast_type`, `or_var`, ... + * `Notation_term` : contains `notation_constr`, was `Topconstr.aconstr` + * `Pattern` : contains `constr_pattern` + * `Tacexpr` : was `tactics/tacexpr.ml` + * `Vernacexpr` : was `toplevel/vernacexpr.ml` - Many files have been divided : - vernacexpr: vernacexpr.mli + Locality - decl_kinds: decl_kinds.mli + Kindops - evd: evar_kinds.mli + evd - tacexpr: tacexpr.mli + tacops - glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops - topconstr: constrexpr.mli + constrexpr_ops - + notation_expr.mli + notation_ops + topconstr - pattern: pattern.mli + patternops - libnames: libnames (qualid, reference) + globnames (global_reference) - egrammar: egramml + egramcoq + * vernacexpr: vernacexpr.mli + Locality + * decl_kinds: decl_kinds.mli + Kindops + * evd: evar_kinds.mli + evd + * tacexpr: tacexpr.mli + tacops + * glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops + * topconstr: constrexpr.mli + constrexpr_ops + + notation_expr.mli + notation_ops + topconstr + * pattern: pattern.mli + patternops + * libnames: libnames (qualid, reference) + globnames (global_reference) + * egrammar: egramml + egramcoq - New utility files : miscops (cf. misctypes.mli) and redops (cf genredexpr.mli). @@ -686,11 +720,11 @@ printing. letin_pat_tac do not accept a type anymore - New file find_subterm.ml for gathering former functions - subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now - take and outputs also an evar_map), and - subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now - renamed into replace_term_occ_modulo and - replace_term_occ_decl_modulo). + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl` (which now + take and outputs also an `evar_map`), and + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl_modulo` (now + renamed into `replace_term_occ_modulo` and + `replace_term_occ_decl_modulo`). - API of Inductiveops made more uniform (see commit log or file itself). @@ -704,36 +738,34 @@ printing. - All functions taking an env and a sigma (or an evdref) now takes the env first. -========================================= -= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = -========================================= +## Changes between Coq 8.3 and Coq 8.4 -** Functions in unification.ml have now the evar_map coming just after the env +- Functions in unification.ml have now the evar_map coming just after the env -** Removal of Tacinterp.constr_of_id ** +- Removal of Tacinterp.constr_of_id Use instead either global_reference or construct_reference in constrintern.ml. -** Optimizing calls to Evd functions ** +- Optimizing calls to Evd functions Evars are split into defined evars and undefined evars; for efficiency, when an evar is known to be undefined, it is preferable to use specific functions about undefined evars since these ones are generally fewer than the defined ones. -** Type changes in TACTIC EXTEND rules ** +- Type changes in TACTIC EXTEND rules Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained via Tacinterp.eval_tactic. -** ARGUMENT EXTEND ** +- ARGUMENT EXTEND It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED in ARGUMENT EXTEND statements. -** Renaming of rawconstr to glob_constr ** +- Renaming of rawconstr to glob_constr The "rawconstr" type has been renamed to "glob_constr" for consistency. The "raw" in everything related to former rawconstr has @@ -743,62 +775,67 @@ scripts to migrate code using Coq's internals, see commits 13743, 2010) in Subversion repository. Contribs have been fixed too, and commit messages there might also be helpful for migrating. -========================================= -= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = -========================================= +## Changes between Coq 8.2 and Coq 8.3 -** Light cleaning in evarutil.ml ** +### Light cleaning in evaruil.ml whd_castappevar is now whd_head_evar obsolete whd_ise disappears -** Restructuration of the syntax of binders ** +### Restructuration of the syntax of binders +``` binders_let -> binders binders_let_fixannot -> binders_fixannot binder_let -> closed_binder (and now covers only bracketed binders) binder was already obsolete and has been removed +``` -** Semantical change of h_induction_destruct ** +### Semantical change of h_induction_destruct Warning, the order of the isrec and evar_flag was inconsistent and has been permuted. Tactic induction_destruct in tactics.ml is unchanged. -** Internal tactics renamed +### Internal tactics renamed There is no more difference between bindings and ebindings. The following tactics are therefore renamed +``` apply_with_ebindings_gen -> apply_with_bindings_gen left_with_ebindings -> left_with_bindings right_with_ebindings -> right_with_bindings split_with_ebindings -> split_with_bindings +``` and the following tactics are removed -apply_with_ebindings (use instead apply_with_bindings) -eapply_with_ebindings (use instead eapply_with_bindings) + - apply_with_ebindings (use instead apply_with_bindings) + - eapply_with_ebindings (use instead eapply_with_bindings) -** Obsolete functions in typing.ml +### Obsolete functions in typing.ml For mtype_of, msort_of, mcheck, now use type_of, sort_of, check -** Renaming functions renamed +### Renaming functions renamed +``` concrete_name -> compute_displayed_name_in concrete_let_name -> compute_displayed_let_name_in rename_rename_bound_var -> rename_bound_vars_as_displayed lookup_name_as_renamed -> lookup_name_as_displayed next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away +``` -** Cleaning in commmand.ml +### Cleaning in commmand.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml Functions renamed: +``` declare_one_assumption -> declare_assumption declare_assumption -> declare_assumptions Command.syntax_definition -> Metasyntax.add_syntactic_definition @@ -815,15 +852,17 @@ instantiate_type_indrec_scheme -> weaken_sort_scheme instantiate_indrec_scheme -> modify_sort_scheme make_case_dep, make_case_nodep -> build_case_analysis_scheme make_case_gen -> build_case_analysis_scheme_default +``` Types: decl_notation -> decl_notation option -** Cleaning in libnames/nametab interfaces +### Cleaning in libnames/nametab interfaces Functions: +``` dirpath_prefix -> pop_dirpath extract_dirpath_prefix pop_dirpath_n extend_dirpath -> add_dirpath_suffix @@ -837,17 +876,19 @@ absolute_reference -> global_of_path locate_syntactic_definition -> locate_syndef path_of_syntactic_definition -> path_of_syndef push_syntactic_definition -> push_syndef +``` Types: section_path -> full_path -** Cleaning in parsing extensions (commit 12108) +### Cleaning in parsing extensions (commit 12108) Many moves and renamings, one new file (Extrawit, that contains wit_tactic). -** Cleaning in tactical.mli +### Cleaning in tactical.mli +``` tclLAST_HYP -> onLastHyp tclLAST_DECL -> onLastDecl tclLAST_NHYPS -> onNLastHypsId @@ -857,24 +898,21 @@ onLastHyp -> onLastHypId onNLastHyps -> onNLastDecls onClauses -> onClause allClauses -> allHypsAndConcl +``` -+ removal of various unused combinators on type "clause" - -========================================= -= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = -========================================= +and removal of various unused combinators on type "clause" -A few differences in Coq ML interfaces between Coq V8.1 and V8.2 -================================================================ +## Changes between Coq 8.1 and Coq 8.2 -** Datatypes +### Datatypes List of occurrences moved from "int list" to "Termops.occurrences" (an alias to "bool * int list") ETIdent renamed to ETName -** Functions +### Functions +``` Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply Tactics: apply_with_bindings -> apply_with_bindings_wo_evars Eauto.simplest_apply -> Hiddentac.h_simplest_apply @@ -884,98 +922,93 @@ Tactics.true_cut renamed into Tactics.assert_tac Constrintern.interp_constrpattern -> intern_constr_pattern Hipattern.match_with_conjunction is a bit more restrictive Hipattern.match_with_disjunction is a bit more restrictive +``` -** Universe names (univ.mli) +### Universe names (univ.mli) + ```ocaml base_univ -> type0_univ (* alias of Set is the Type hierarchy *) prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) is_base_univ -> is_type1_univ is_empty_univ -> is_lower_univ + ``` -** Sort names (term.mli) +### Sort names (term.mli) + ``` mk_Set -> set_sort mk_Prop -> prop_sort type_0 -> type1_sort - -========================================= -= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.0 and V8.1 -================================================================ - -** Functions - -Util: option_app -> option_map -Term: substl_decl -> subst_named_decl -Lib: library_part -> remove_section_part -Printer: prterm -> pr_lconstr -Printer: prterm_env -> pr_lconstr_env -Ppconstr: pr_sort -> pr_rawsort -Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) -Pretyping: - - understand_gen_tcc and understand_gen_ltac merged into understand_ltac - - type_constraints can now say typed by a sort (use OfType to get the - previous behavior) -Library: import_library -> import_module - -** Constructors - -Declarations: mind_consnrealargs -> mind_consnrealdecls -NoRedun -> NoDup -Cast and RCast have an extra argument: you can recover the previous + ``` + +## Changes between Coq 8.0 and Coq 8.1 + +### Functions + +- Util: option_app -> option_map +- Term: substl_decl -> subst_named_decl +- Lib: library_part -> remove_section_part +- Printer: prterm -> pr_lconstr +- Printer: prterm_env -> pr_lconstr_env +- Ppconstr: pr_sort -> pr_rawsort +- Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) +- Pretyping: + - understand_gen_tcc and understand_gen_ltac merged into understand_ltac + - type_constraints can now say typed by a sort (use OfType to get the + previous behavior) +- Library: import_library -> import_module + +### Constructors + + * Declarations: mind_consnrealargs -> mind_consnrealdecls + * NoRedun -> NoDup + * Cast and RCast have an extra argument: you can recover the previous behavior by setting the extra argument to "CastConv DEFAULTcast" and "DEFAULTcast" respectively -Names: "kernel_name" is now "constant" when argument of Term.Const -Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert -Tacexpr: TacForward(true,_,_) branched to TacLetTac + * Names: "kernel_name" is now "constant" when argument of Term.Const + * Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert + * Tacexpr: TacForward(true,_,_) branched to TacLetTac -** Modules +### Modules -module Decl_kinds: new interface -module Bigint: new interface -module Tacred spawned module Redexpr -module Symbols -> Notation -module Coqast, Ast, Esyntax, Termast, and all other modules related to old - syntax are removed -module Instantiate: integrated to Evd -module Pretyping now a functor: use Pretyping.Default instead + * module Decl_kinds: new interface + * module Bigint: new interface + * module Tacred spawned module Redexpr + * module Symbols -> Notation + * module Coqast, Ast, Esyntax, Termast, and all other modules related to old + syntax are removed + * module Instantiate: integrated to Evd + * module Pretyping now a functor: use Pretyping.Default instead -** Internal names +### Internal names OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE -** Tactic extensions +### Tactic extensions -- printers have an extra parameter which is a constr printer at high precedence -- the tactic printers have an extra arg which is the expected precedence -- level is now a precedence in declare_extra_tactic_pprule -- "interp" functions now of types the actual arg type, not its encapsulation - as a generic_argument + * printers have an extra parameter which is a constr printer at high precedence + * the tactic printers have an extra arg which is the expected precedence + * level is now a precedence in declare_extra_tactic_pprule + * "interp" functions now of types the actual arg type, not its encapsulation + as a generic_argument -========================================= -= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 = -========================================= +## Changes between Coq 7.4 and Coq 8.0 See files in dev/syntax-v8 -============================================== -= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 = -============================================== +## Main changes between Coq 7.4 and Coq 8.0 -CHANGES DUE TO INTRODUCTION OF MODULES -====================================== +### Changes due to introduction of modules -1.Kernel --------- +#### Kernel The module level has no effect on constr except for the structure of section_path. The type of unique names for constructions (what section_path served) is now called a kernel name and is defined by +```ocaml type uniq_ident = int * string * dir_path (* int may be enough *) type module_path = | MPfile of dir_path (* reference to physical module, e.g. file *) @@ -1002,7 +1035,8 @@ type kernel_name = module_path * dir_path * label Def u = ... end Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a - +``` + <M> and <N> are self-references, X is a bound reference and L is a reference to a physical module. @@ -1019,14 +1053,13 @@ world. module_expr) and kernel/declarations.ml (type module_body and module_type_body). -2. Library ----------- +#### Library -i) tables +1. tables [Summaries] - the only change is the special treatment of the global environmet. -ii) objects +2. objects [Libobject] declares persistent objects, given with methods: * cache_function specifying how to add the object in the current @@ -1047,25 +1080,25 @@ Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal version such as (MPself<Datatypes#1>,[],"Fst") (see above) -What happens at the end of an interactive module ? -================================================== +#### What happens at the end of an interactive module ? + (or when a file is stored and reloaded from disk) All summaries (except Global environment) are reverted to the state from before the beginning of the module, and: -a) the objects (again, since last Declaremods.start_module or +1. the objects (again, since last Declaremods.start_module or Library.start_library) are classified using the classify_function. To simplify consider only those who returned Substitute _ or Keep _. -b) If the module is not a functor, the subst_function for each object of +2. If the module is not a functor, the subst_function for each object of the first group is called with the substitution [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"]. Then the load_function is called for substituted objects and the "keep" object. (If the module is a library the substitution is done at reloading). -c) The objects which returned substitute are stored in the modtab +3. The objects which returned substitute are stored in the modtab together with the self ident of the module, and functor argument names if the module was a functor. @@ -1075,9 +1108,9 @@ c) The objects which returned substitute are stored in the modtab is evaluated -The difference between "substitute" and "keep" objects -======================================================== -i) The "keep" objects can _only_ reference other objects by section_paths +#### The difference between "substitute" and "keep" objects + +1. The "keep" objects can _only_ reference other objects by section_paths and qualids. They do not need the substitution function. They will work after end_module (or reloading a compiled library), @@ -1089,7 +1122,7 @@ These would typically be grammar rules, pretty printing rules etc. -ii) The "substitute" objects can _only_ reference objects by +2. The "substitute" objects can _only_ reference objects by kernel_names. They must have a valid subst_function. They will work after end_module _and_ after Module Z:=N or @@ -1098,17 +1131,18 @@ Module Z:=F(M). Other kinds of objects: -iii) "Dispose" - objects which do not survive end_module + +3. "Dispose" - objects which do not survive end_module As a consequence, objects which reference other objects sometimes by kernel_names and sometimes by section_path must be of this kind... -iv) "Anticipate" - objects which must be treated individually by +4. "Anticipate" - objects which must be treated individually by end_module (typically "REQUIRE" objects) -Writing subst_thing functions -============================= +#### Writing subst_thing functions + The subst_thing shoud not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. @@ -1123,15 +1157,13 @@ They are all (apart from constr, for now) written in the non-copying way. -Nametab -======= +#### Nametab Nametab has been made more uniform. For every kind of thing there is only one "push" function and one "locate" function. -Lib -=== +#### Lib library_segment is now a list of object_name * library_item, where object_name = section_path * kernel_name (see above) @@ -1139,20 +1171,19 @@ object_name = section_path * kernel_name (see above) New items have been added for open modules and module types -Declaremods -========== +#### Declaremods + Functions to declare interactive and noninteractive modules and module types. -Library -======= +#### Library + Uses Declaremods to actually communicate with Global and to register objects. -OTHER CHANGES -============= +### Other changes Internal representation of tactics bindings has changed (see type Rawterm.substitution). @@ -1169,258 +1200,48 @@ New parsing model for tactics and vernacular commands TACTIC EXTEND ... END to be used in ML files New organisation of THENS: -tclTHENS tac tacs : tacs is now an array -tclTHENSFIRSTn tac1 tacs tac2 : + +- tclTHENS tac tacs : tacs is now an array +- tclTHENSFIRSTn tac1 tacs tac2 : apply tac1 then, apply the array tacs on the first n subgoals and tac2 on the remaining subgoals (previously tclTHENST) -tclTHENSLASTn tac1 tac2 tacs : +- tclTHENSLASTn tac1 tac2 tacs : apply tac1 then, apply tac2 on the first subgoals and apply the array tacs on the last n subgoals -tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) -tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs -tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] -tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) -tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") -tclTHENSV same as tclTHENS but with an array -tclTHENSi : no longer available +- tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) +- tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs +- tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] +- tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) +- tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") +- tclTHENSV same as tclTHENS but with an array +- tclTHENSi : no longer available Proof_type: subproof field in type proof_tree glued with the ref field Tacmach: no more echo from functions of module Refiner Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. + Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd VERNAC COMMAND EXTEND macros + File syntax/PPTactic.v moved to parsing/pptactic.ml + Tactics about False and not now in tactics/contradiction.ml + Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) + File tacinterp.ml moved from proofs to directory tactics -========================================== -= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 = -========================================== +## Changes between Coq 7.1 and Coq 7.2 The core of Coq (kernel) has meen minimized with the following effects: -kernel/term.ml split into kernel/term.ml, pretyping/termops.ml -kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml -kernel/names.ml split into kernel/names.ml, library/nameops.ml -kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml +- kernel/term.ml split into kernel/term.ml, pretyping/termops.ml +- kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml +- kernel/names.ml split into kernel/names.ml, library/nameops.ml +- kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors, e.g. IsRel is now Rel, IsMutCase is now Case, etc. - - -======================================================= -= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 = -======================================================= - -Changements d'organisation / modules : --------------------------------------- - - Std, More_util -> lib/util.ml - - Names -> kernel/names.ml et kernel/sign.ml - (les parties noms et signatures ont été séparées) - - Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) - Mhb -> Bij - - Generic est intégré à Term (et un petit peu à Closure) - -Changements dans les types de données : ---------------------------------------- - dans Generic: free_rels : constr -> int Listset.t - devient : constr -> Intset.t - - type_judgement -> typed_type - environment -> context - context -> typed_type signature - - -ATTENTION: ----------- - - Il y a maintenant d'autres exceptions que UserError (TypeError, - RefinerError, etc.) - - Il ne faut donc plus se contenter (pour rattraper) de faire - - try . .. with UserError _ -> ... - - mais écrire à la place - - try ... with e when Logic.catchable_exception e -> ... - - -Changements dans les fonctions : --------------------------------- - - Vectops. - it_vect -> Array.fold_left - vect_it -> Array.fold_right - exists_vect -> Util.array_exists - for_all2eq_vect -> Util.array_for_all2 - tabulate_vect -> Array.init - hd_vect -> Util.array_hd - tl_vect -> Util.array_tl - last_vect -> Util.array_last - it_vect_from -> array_fold_left_from - vect_it_from -> array_fold_right_from - app_tl_vect -> array_app_tl - cons_vect -> array_cons - map_i_vect -> Array.mapi - map2_vect -> array_map2 - list_of_tl_vect -> array_list_of_tl - - Names - sign_it -> fold_var_context (se fait sur env maintenant) - it_sign -> fold_var_context_reverse (sur env maintenant) - - Generic - noccur_bet -> noccur_between - substn_many -> substnl - - Std - comp -> Util.compose - rev_append -> List.rev_append - - Termenv - mind_specif_of_mind -> Global.lookup_mind_specif - ou Environ.lookup_mind_specif si on a un env sous la main - mis_arity -> instantiate_arity - mis_lc -> instantiate_lc - - Ex-Environ - mind_of_path -> Global.lookup_mind - - Printer - gentermpr -> gen_pr_term - term0 -> prterm_env - pr_sign -> pr_var_context - pr_context_opt -> pr_context_of - pr_ne_env -> pr_ne_context_of - - Typing, Machops - type_of_type -> judge_of_type - fcn_proposition -> judge_of_prop_contents - safe_fmachine -> safe_infer - - Reduction, Clenv - whd_betadeltat -> whd_betaevar - whd_betadeltatiota -> whd_betaiotaevar - find_mrectype -> Inductive.find_mrectype - find_minductype -> Inductive.find_inductive - find_mcoinductype -> Inductive.find_coinductive - - Astterm - constr_of_com_casted -> interp_casted_constr - constr_of_com_sort -> interp_type - constr_of_com -> interp_constr - rawconstr_of_com -> interp_rawconstr - type_of_com -> type_judgement_of_rawconstr - judgement_of_com -> judgement_of_rawconstr - - Termast - bdize -> ast_of_constr - - Tacmach - pf_constr_of_com_sort -> pf_interp_type - pf_constr_of_com -> pf_interp_constr - pf_get_hyp -> pf_get_hyp_typ - pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant) - - Pattern - raw_sopattern_of_compattern -> Astterm.interp_constrpattern - somatch -> is_matching - dest_somatch -> matches - - Tacticals - matches -> gl_is_matching - dest_match -> gl_matches - suff -> utiliser sort_of_goal - lookup_eliminator -> utiliser sort_of_goal pour le dernier arg - - Divers - initial_sign -> var_context - - Sign - ids_of_sign -> ids_of_var_context (or Environ.ids_of_context) - empty_sign -> empty_var_context - - Pfedit - list_proofs -> get_all_proof_names - get_proof -> get_current_proof_name - abort_goal -> abort_proof - abort_goals -> abort_all_proofs - abort_cur_goal -> abort_current_proof - get_evmap_sign -> get_goal_context/get_current_goal_context - unset_undo -> reset_undo - - Proof_trees - mkGOAL -> mk_goal - - Declare - machine_constant -> declare_constant (+ modifs) - - ex-Trad, maintenant Pretyping - inh_cast_rel -> Coercion.inh_conv_coerce_to - inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail - ise_resolve1 -> understand, understand_type - ise_resolve -> understand_judgment, understand_type_judgment - - ex-Tradevar, maintenant Evarutil - mt_tycon -> empty_tycon - - Recordops - struc_info -> find_structure - -Changements dans les inductifs ------------------------------- -Nouveaux types "constructor" et "inductive" dans Term -La plupart des fonctions de typage des inductives prennent maintenant -un inductive au lieu d'un oonstr comme argument. Les seules fonctions -à traduire un constr en inductive sont les find_rectype and co. - -Changements dans les grammaires -------------------------------- - - . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex - - . attention : LIDENT -> IDENT (les identificateurs n'ont pas de - casse particulière dans Coq) - - . Le mot "command" est remplacé par "constr" dans les noms de - fichiers, noms de modules et non-terminaux relatifs au parsing des - termes; aussi les changements suivants "COMMAND"/"CONSTR" dans - g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml* - - . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n - passent en minuscule Identifier, Constr, ... - - . Plusieurs parsers ont changé de format (ex: sortarg) - -Changements dans le pretty-printing ------------------------------------ - - . Découplage de la traduction de constr -> rawconstr (dans detyping) - et de rawconstr -> ast (dans termast) - . Déplacement des options d'affichage de printer vers termast - . Déplacement des réaiguillage d'univers du pp de printer vers esyntax - - -Changements divers ------------------- - - . il n'y a plus de script coqtop => coqtop et coqtop.byte sont - directement le résultat du link du code - => debuggage et profiling directs - - . il n'y a plus d'installation locale dans bin/$ARCH - - . #use "include.ml" => #use "include" - go() => loop() - - . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup - de temps diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 364fc883ba..9be70e6d38 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -463,7 +463,7 @@ object(self) self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> - log_pp ?id Pp.(str "ErrorMsg" ++ msg); + log_pp ?id Pp.(str "ErrorMsg " ++ msg); remove_flag sentence `PROCESSING; let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`ERROR (loc, rmsg)); @@ -471,17 +471,17 @@ object(self) self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> - log_pp ?id Pp.(str "WarningMsg" ++ msg); + log_pp ?id Pp.(str "WarningMsg " ++ msg); let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log_pp ?id Pp.(str "Msg" ++ msg); + log_pp ?id Pp.(str "Msg " ++ msg); messages#push lvl msg | Message(lvl, loc, msg), None -> - log_pp Pp.(str "Msg" ++ msg); + log_pp Pp.(str "Msg " ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n diff --git a/ide/coqide.ml b/ide/coqide.ml index 7b65c9fec9..2c8ce0049e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -439,7 +439,9 @@ let compile sn = match sn.fileops#filename with |None -> flash_info "Active buffer has no name" |Some f -> - let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f)) + let args = Coq.get_arguments sn.coqtop in + let cmd = cmd_coqc#get + ^ " " ^ String.concat " " args ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 67391f5567..b11a11606f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,5 +1,4 @@ (************************************************************************) - (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 2d0a19b9a6..771c137344 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -320,13 +320,13 @@ let coerce_reference_to_id = function (str "This expression should be a simple identifier.") let coerce_to_id = function - | { CAst.v = CRef (Ident (loc,id),_); _ } -> (loc,id) + | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id) | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id) - | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous) + | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id) + | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous) | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") diff --git a/interp/notation.ml b/interp/notation.ml index 176ac3bf68..d3cac1e3e9 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -425,7 +425,7 @@ let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" (fun (ntn,which_scope) -> str "Notation" ++ spc () ++ str ntn ++ spc () - ++ strbrk "was already used" ++ which_scope) + ++ strbrk "was already used" ++ which_scope ++ str ".") let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0341167318..3d48114ec6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -297,28 +297,29 @@ let compare_recursive_parts found f f' (iterator,subc) = user_err ?loc:(subtract_loc loc1 loc2) (str "Both ends of the recursive pattern are the same.") | Some (x,y,RecursiveTerms lassoc) -> - let newfound,x,y,lassoc = + let toadd,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) then - !found,x,y,lassoc + None,x,y,lassoc else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) then - !found,y,x,not lassoc + None,y,x,not lassoc else - (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in + Some (x,y),x,y,lassoc in let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in - (* found have been collected by compare_constr *) - found := newfound; + (* found variables have been collected by compare_constr *) + found := (List.remove Id.equal y (pi1 !found), + Option.fold_right (fun a l -> a::l) toadd (pi2 !found), + pi3 !found); NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (t_x,t_y)) -> - let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) - found := newfound; + found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found); check_is_hole x t_x; check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) @@ -348,7 +349,7 @@ let notation_constr_and_vars_of_glob_constr a = | _c -> aux' c and aux' x = DAst.with_val (function - | GVar id -> add_id found id; NVar id + | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id | GApp (g,args) -> NApp (aux g, List.map aux args) | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) @@ -823,7 +824,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) alp, b :: bl | _ -> raise No_match in let alp, bl = unify alp bl bl' in - let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in alp, add_bindinglist_env sigma var bl with Not_found -> alp, add_bindinglist_env sigma var bl @@ -909,7 +910,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc | GLambda (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) - when islambda && is_gvar p e -> + when islambda && is_gvar p e && not (occur_glob_constr p b) -> match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b | _, _ when islambda -> match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b @@ -918,7 +919,7 @@ let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc | GProd (na,bk,t,b) as b0 -> begin match na, DAst.get b with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))]) - when not islambda && is_gvar p e -> + when not islambda && is_gvar p e && not (occur_glob_constr p b) -> match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b | Name _, _ when not islambda -> match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b @@ -991,8 +992,6 @@ let does_not_come_from_already_eta_expanded_var glob = (* checked). *) match DAst.get glob with GVar _ -> false | _ -> true -let is_var c = match DAst.get c with GVar _ -> true | _ -> false - let rec match_ inner u alp metas sigma a1 a2 = let open CAst in let loc = a1.loc in @@ -1009,7 +1008,8 @@ let rec match_ inner u alp metas sigma a1 a2 = | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> begin match na1, DAst.get b1, iter with (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e -> + | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) + when is_gvar p e && not (occur_glob_constr p b1) -> let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin @@ -1027,7 +1027,8 @@ let rec match_ inner u alp metas sigma a1 a2 = | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) -> (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) begin match na1, DAst.get b1, iter, termin with - | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e -> + | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ + when is_gvar p e && not (occur_glob_constr p b1) -> let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin @@ -1049,7 +1050,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) -> begin match na1, DAst.get b1, na2 with | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id - when is_var e && is_bindinglist_meta id metas -> + when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) -> let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in match_in u alp metas sigma b1 b2 | _, _, Name id when is_bindinglist_meta id metas -> diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 274ea6213b..45dec5112b 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -50,6 +50,8 @@ let wit_ref = make0 "ref" let wit_quant_hyp = make0 "quant_hyp" +let wit_sort_family = make0 "sort_family" + let wit_constr = make0 "constr" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 1d4a29b9c2..dffbd6659f 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -47,6 +47,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type +val wit_sort_family : (Sorts.family, unit, unit) genarg_type + val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 2adf522b74..a02f1a9d4e 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -169,7 +169,7 @@ type option_ref_value = (** Identifier and optional list of bound universes. *) type plident = lident * lident list option -type sort_expr = glob_sort +type sort_expr = Sorts.family type definition_expr = | ProveBody of local_binder_expr list * constr_expr diff --git a/kernel/univ.ml b/kernel/univ.ml index d915fb8c98..bae782f5d4 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -31,133 +31,6 @@ open Util union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -module type Hashconsed = -sig - type t - val hash : t -> int - val eq : t -> t -> bool - val hcons : t -> t -end - -module HashedList (M : Hashconsed) : -sig - type t = private Nil | Cons of M.t * int * t - val nil : t - val cons : M.t -> t -> t -end = -struct - type t = Nil | Cons of M.t * int * t - module Self = - struct - type _t = t - type t = _t - type u = (M.t -> M.t) - let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 - | _ -> false - let hashcons hc = function - | Nil -> Nil - | Cons (x, h, l) -> Cons (hc x, h, l) - end - module Hcons = Hashcons.Make(Self) - let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons - (** No recursive call: the interface guarantees that all HLists from this - program are already hashconsed. If we get some external HList, we can - still reconstruct it by traversing it entirely. *) - let nil = Nil - let cons x l = - let h = M.hash x in - let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in - let h = Hashset.Combine.combine h hl in - hcons (Cons (x, h, l)) -end - -module HList = struct - - module type S = sig - type elt - type t = private Nil | Cons of elt * int * t - val hash : t -> int - val nil : t - val cons : elt -> t -> t - val tip : elt -> t - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val map : (elt -> elt) -> t -> t - val smartmap : (elt -> elt) -> t -> t - val exists : (elt -> bool) -> t -> bool - val for_all : (elt -> bool) -> t -> bool - val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val mem : elt -> t -> bool - val remove : elt -> t -> t - val to_list : t -> elt list - val compare : (elt -> elt -> int) -> t -> t -> int - end - - module Make (H : Hashconsed) : S with type elt = H.t = - struct - type elt = H.t - include HashedList(H) - - let hash = function Nil -> 0 | Cons (_, h, _) -> h - - let tip e = cons e nil - - let rec fold f l accu = match l with - | Nil -> accu - | Cons (x, _, l) -> fold f l (f x accu) - - let rec map f = function - | Nil -> nil - | Cons (x, _, l) -> cons (f x) (map f l) - - let smartmap = map - (** Apriori hashconsing ensures that the map is equal to its argument *) - - let rec exists f = function - | Nil -> false - | Cons (x, _, l) -> f x || exists f l - - let rec for_all f = function - | Nil -> true - | Cons (x, _, l) -> f x && for_all f l - - let rec for_all2 f l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2 - | _ -> false - - let rec to_list = function - | Nil -> [] - | Cons (x, _, l) -> x :: to_list l - - let rec remove x = function - | Nil -> nil - | Cons (y, _, l) -> - if H.eq x y then l - else cons y (remove x l) - - let rec mem x = function - | Nil -> false - | Cons (y, _, l) -> H.eq x y || mem x l - - let rec compare cmp l1 l2 = match l1, l2 with - | Nil, Nil -> 0 - | Cons (x1, h1, l1), Cons (x2, h2, l2) -> - let c = Int.compare h1 h2 in - if c == 0 then - let c = cmp x1 x2 in - if c == 0 then - compare cmp l1 l2 - else c - else c - | Cons _, Nil -> 1 - | Nil, Cons _ -> -1 - - end -end - module RawLevel = struct open Names @@ -390,12 +263,11 @@ struct module Expr = struct type t = Level.t * int - type _t = t (* Hashing of expressions *) module ExprHash = struct - type t = _t + type t = Level.t * int type u = Level.t -> Level.t let hashcons hdir (b,n as x) = let b' = hdir b in @@ -409,25 +281,12 @@ struct end - module HExpr = - struct - - module H = Hashcons.Make(ExprHash) - - type t = ExprHash.t - - let hcons = - Hashcons.simple_hcons H.generate H.hcons Level.hcons - let hash = ExprHash.hash - let eq x y = x == y || - (let (u,n) = x and (v,n') = y in - Int.equal n n' && Level.equal u v) - - end + module H = Hashcons.Make(ExprHash) - let hcons = HExpr.hcons + let hcons = + Hashcons.simple_hcons H.generate H.hcons Level.hcons - let make l = hcons (l, 0) + let make l = (l, 0) let compare u v = if u == v then 0 @@ -436,8 +295,8 @@ struct if Int.equal n n' then Level.compare x x' else n - n' - let prop = make Level.prop - let set = make Level.set + let prop = hcons (Level.prop, 0) + let set = hcons (Level.set, 0) let type1 = hcons (Level.set, 1) let is_small = function @@ -448,6 +307,8 @@ struct (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) + let hash = ExprHash.hash + let leq (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then n <= n' @@ -457,13 +318,13 @@ struct let successor (u,n) = if Level.is_prop u then type1 - else hcons (u, n + 1) + else (u, n + 1) let addn k (u,n as x) = if k = 0 then x else if Level.is_prop u then - hcons (Level.set,n+k) - else hcons (u,n+k) + (Level.set,n+k) + else (u,n+k) type super_result = SuperSame of bool @@ -515,71 +376,63 @@ struct let v' = f v in if v' == v then x else if Level.is_prop v' && n != 0 then - hcons (Level.set, n) - else hcons (v', n) + (Level.set, n) + else (v', n) end - - let compare_expr = Expr.compare - module Huniv = HList.Make(Expr.HExpr) - type t = Huniv.t - open Huniv - - let equal x y = x == y || - (Huniv.hash x == Huniv.hash y && - Huniv.for_all2 Expr.equal x y) + type t = Expr.t list - let hash = Huniv.hash + let tip l = [l] + let cons x l = x :: l - let compare x y = - if x == y then 0 - else - let hx = Huniv.hash x and hy = Huniv.hash y in - let c = Int.compare hx hy in - if c == 0 then - Huniv.compare (fun e1 e2 -> compare_expr e1 e2) x y - else c + let rec hash = function + | [] -> 0 + | e :: l -> Hashset.Combine.combinesmall (Expr.ExprHash.hash e) (hash l) + + let equal x y = x == y || List.equal Expr.equal x y + + let compare x y = if x == y then 0 else List.compare Expr.compare x y + + module Huniv = Hashcons.Hlist(Expr) - let rec hcons = function - | Nil -> Huniv.nil - | Cons (x, _, l) -> Huniv.cons x (hcons l) + let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons - let make l = Huniv.tip (Expr.make l) - let tip x = Huniv.tip x + let make l = tip (Expr.make l) + let tip x = tip x let pr l = match l with - | Cons (u, _, Nil) -> Expr.pr u + | [u] -> Expr.pr u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ + (prlist_with_sep pr_comma Expr.pr l) ++ str ")" let pr_with f l = match l with - | Cons (u, _, Nil) -> Expr.pr_with f u + | [u] -> Expr.pr_with f u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++ + (prlist_with_sep pr_comma (Expr.pr_with f) l) ++ str ")" let is_level l = match l with - | Cons (l, _, Nil) -> Expr.is_level l + | [l] -> Expr.is_level l | _ -> false let rec is_levels l = match l with - | Cons (l, _, r) -> Expr.is_level l && is_levels r - | Nil -> true + | l :: r -> Expr.is_level l && is_levels r + | [] -> true let level l = match l with - | Cons (l, _, Nil) -> Expr.level l + | [l] -> Expr.level l | _ -> None let levels l = - fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty + List.fold_left (fun acc x -> LSet.add (Expr.get_level x) acc) LSet.empty l let is_small u = match u with - | Cons (l, _, Nil) -> Expr.is_small l + | [l] -> Expr.is_small l | _ -> false (* The lower predicative level of the hierarchy that contains (impredicative) @@ -601,16 +454,16 @@ struct let super l = if is_small l then type1 else - Huniv.map (fun x -> Expr.successor x) l + List.smartmap (fun x -> Expr.successor x) l let addn n l = - Huniv.map (fun x -> Expr.addn n x) l + List.smartmap (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons (h1, _, t1), Cons (h2, _, t2) -> + | [], _ -> l2 + | _, [] -> l1 + | h1 :: t1, h2 :: t2 -> let open Expr in (match super h1 h2 with | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 @@ -623,7 +476,7 @@ struct let sort u = let rec aux a l = match l with - | Cons (b, _, l') -> + | b :: l' -> let open Expr in (match super a b with | SuperSame false -> aux a l' @@ -631,21 +484,21 @@ struct | SuperDiff c -> if c <= 0 then cons a l else cons b (aux a l')) - | Nil -> cons a l + | [] -> cons a l in - fold (fun a acc -> aux a acc) u nil + List.fold_right (fun a acc -> aux a acc) u [] (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y - let empty = nil + let empty = [] - let exists = Huniv.exists + let exists = List.exists - let for_all = Huniv.for_all + let for_all = List.for_all - let smartmap = Huniv.smartmap + let smartmap = List.smartmap end @@ -818,12 +671,11 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - let open Universe.Huniv in let rec aux acc v = match v with - | Cons (v, _, l) -> - aux (fold (fun u -> constraint_add_leq u v) u c) l - | Nil -> acc + | v :: l -> + aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l + | [] -> acc in aux c v let enforce_leq u v c = @@ -842,12 +694,13 @@ let enforce_univ_constraint (u,d,v) = (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) -let univ_level_mem u v = Huniv.mem (Expr.make u) v +let univ_level_mem u v = + List.exists (fun (l, n) -> Int.equal n 0 && Level.equal u l) v let univ_level_rem u v min = match Universe.level v with | Some u' -> if Level.equal u u' then min else v - | None -> Huniv.remove (Universe.Expr.make u) v + | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v (* Is u mentionned in v (or equals to v) ? *) @@ -1260,7 +1113,7 @@ let subst_univs_expr_opt fn (l,n) = let subst_univs_universe fn ul = let subst, nosubst = - Universe.Huniv.fold (fun u (subst,nosubst) -> + List.fold_right (fun u (subst,nosubst) -> try let a' = subst_univs_expr_opt fn u in (a' :: subst, nosubst) with Not_found -> (subst, u :: nosubst)) @@ -1271,7 +1124,7 @@ let subst_univs_universe fn ul = let substs = List.fold_left Universe.merge_univs Universe.empty subst in - List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) + List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst let subst_univs_level fn l = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f637e9746c..7d0728458b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -123,8 +123,8 @@ let name_colon = let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort global - constr_pattern lconstr_pattern Constr.ident + GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: @@ -149,6 +149,12 @@ GEXTEND Gram | "Type"; "@{"; u = universe; "}" -> GType u ] ] ; + sort_family: + [ [ "Set" -> Sorts.InSet + | "Prop" -> Sorts.InProp + | "Type" -> Sorts.InType + ] ] + ; universe: [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids | id = name -> [id] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 560a9a7578..5b044d2f04 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -64,20 +64,6 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") -let extraction_err ~loc = - if not (Mltop.module_is_known "extraction_plugin") then - CErrors.user_err ~loc (str "Please do first a Require Extraction.") - else - (* The right grammar entries should have been loaded. - We could only end here in case of syntax error. *) - raise (Stream.Error "unexpected end of command") - -let funind_err ~loc = - if not (Mltop.module_is_known "recdef_plugin") then - CErrors.user_err ~loc (str "Please do first a Require Import FunInd.") - else - raise (Stream.Error "unexpected end of command") (* Same as above... *) - GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf; vernac: FIRST @@ -354,13 +340,13 @@ GEXTEND Gram ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) | IDENT "Elimination"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) | IDENT "Case"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) @@ -881,22 +867,6 @@ GEXTEND Gram | IDENT "DelPath"; dir = ne_string -> VernacRemoveLoadPath dir - (* Some plugins are not loaded initially anymore : extraction, - and funind. To ease this transition toward a mandatory Require, - we hack here the vernac grammar in order to get customized - error messages telling what to Require instead of the dreadful - "Illegal begin of vernac". Normally, these fake grammar entries - are overloaded later by the grammar extensions in these plugins. - This code is meant to be removed in a few releases, when this - transition is considered finished. *) - - | IDENT "Extraction" -> extraction_err ~loc:!@loc - | IDENT "Extract" -> extraction_err ~loc:!@loc - | IDENT "Recursive"; IDENT "Extraction" -> extraction_err ~loc:!@loc - | IDENT "Separate"; IDENT "Extraction" -> extraction_err ~loc:!@loc - | IDENT "Function" -> funind_err ~loc:!@loc - | IDENT "Functional" -> funind_err ~loc:!@loc - (* Type-Checking (pas dans le refman) *) | "Type"; c = lconstr -> VernacGlobalCheck c diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 81f02bf955..0d24599eae 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -471,6 +471,7 @@ module Constr = let global = make_gen_entry uconstr "global" let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" + let sort_family = make_gen_entry uconstr "sort_family" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" @@ -631,6 +632,7 @@ let () = Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); Grammar.register0 wit_red_expr (Vernac_.red_expr); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 445818e130..897e42c303 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -225,6 +225,7 @@ module Constr : val global : reference Gram.entry val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry + val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v index 0d5a93b034..d1046ae79b 100644 --- a/plugins/derive/Derive.v +++ b/plugins/derive/Derive.v @@ -1 +1 @@ -Declare ML Module "derive_plugin".
\ No newline at end of file +Declare ML Module "derive_plugin". diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index fabe9a4c67..09b0444614 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -34,4 +34,4 @@ Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". -Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file +Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index fe6eb7780f..ab13d75ada 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -96,4 +96,4 @@ Extraction "/tmp/test.ml" pos_of_int int_of_pos z_of_int int_of_z n_of_int int_of_n. -*)
\ No newline at end of file +*) diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v index 1374a91abf..b3f9d6556d 100644 --- a/plugins/extraction/Extraction.v +++ b/plugins/extraction/Extraction.v @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Declare ML Module "extraction_plugin".
\ No newline at end of file +Declare ML Module "extraction_plugin". diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 513fce2484..ef1654fdf5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -11,7 +11,6 @@ open Tactics open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs -open Misctypes module RelDecl = Context.Rel.Declaration @@ -463,7 +462,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -500,7 +499,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x ) fas in @@ -674,7 +673,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) + Universes.new_sort_in_family x ) fa in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 5a7ffe0590..2eb1b7935d 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -8,7 +8,6 @@ open Names open Term -open Misctypes val generate_functional_principle : Evd.evar_map ref -> @@ -37,8 +36,7 @@ val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list - -val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit + (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list +val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 16d9f200f3..62ecaa552b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,11 +166,11 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_glob_sort s + Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ] END diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8dea6c90f5..5f8d50da12 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -797,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( (fun entry -> (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) ) - (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs)) + (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) ) in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 99e4440102..b4c6f9c90e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -403,38 +403,38 @@ open Leminv let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater -VERNAC ARGUMENT EXTEND sort -| [ "Set" ] -> [ GSet ] -| [ "Prop" ] -> [ GProp ] -| [ "Type" ] -> [ GType [] ] -END +(*VERNAC ARGUMENT EXTEND sort_family +| [ "Set" ] -> [ InSet ] +| [ "Prop" ] -> [ InProp ] +| [ "Type" ] -> [ InType ] +END*) VERNAC COMMAND EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ] END VERNAC COMMAND EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c GProp false inv_tac ] + -> [ add_inversion_lemma_exn na c InProp false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] +| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] END diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v index 3ddb6bed12..657aae90e8 100644 --- a/plugins/romega/ROmega.v +++ b/plugins/romega/ROmega.v @@ -11,4 +11,4 @@ Require Export Setoid. Require Export PreOmega. Require Export ZArith_base. Require Import OmegaPlugin. -Declare ML Module "romega_plugin".
\ No newline at end of file +Declare ML Module "romega_plugin". diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 329fa0ee81..36d1e7c542 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -460,4 +460,4 @@ Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H intro H'; move H' after H; clear H;rename H' into H; - unfold g;clear g.
\ No newline at end of file + unfold g;clear g. diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886cfd880f..ca7f633dc5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -90,7 +90,8 @@ let rec build_lambda sigma vars ctx m = match vars with let pre, suf = List.chop (pred n) ctx in let (na, t, suf) = match suf with | [] -> assert false - | (_, na, t) :: suf -> (na, t, suf) + | (_, id, t) :: suf -> + (Name id, t, suf) in (** Check that the abstraction is legal by generating a transitive closure of its dependencies. *) @@ -126,11 +127,11 @@ let rec build_lambda sigma vars ctx m = match vars with mkRel 1 :: List.mapi (fun i _ -> mkRel (i + keep + 2)) suf in - let map i (id, na, c) = + let map i (na, id, c) = let i = succ i in let subst = List.skipn i subst in let subst = List.map (fun c -> Vars.lift (- i) c) subst in - (id, na, substl subst c) + (na, id, substl subst c) in let pre = List.mapi map pre in let pre = List.filter_with clear pre in @@ -150,11 +151,10 @@ let rec build_lambda sigma vars ctx m = match vars with let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu -| (na1, na2, _) :: ctx -> +| (na, _, _) :: ctx -> if Int.Set.mem k frels then - begin match na1 with + begin match na with | Name id -> - let () = assert (match na2 with Anonymous -> false | Name _ -> true) in let () = if Id.Set.mem id accu then raise PatternMatchingFailure in extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx | Anonymous -> raise PatternMatchingFailure @@ -167,13 +167,21 @@ let extract_bound_vars frels ctx = let dummy_constr = EConstr.mkProp let make_renaming ids = function -| (Name id, Name _, _) -> +| (Name id, _, _) -> begin try EConstr.mkRel (List.index Id.equal id ids) with Not_found -> dummy_constr end | _ -> dummy_constr +let push_binder na1 na2 t ctx = + let id2 = match na2 with + | Name id2 -> id2 + | Anonymous -> + let avoid = List.map pi2 ctx in + 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)) @@ -306,19 +314,19 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> @@ -327,7 +335,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then - let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in + let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = push_binder Anonymous na t l in let ctx_br = List.fold_left f ctx ctx_b2 in let ctx_br' = List.fold_left f ctx ctx_b2' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 79d2c3333b..7cd35f530a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -222,18 +222,6 @@ let interp_level_info ?loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ?loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) -let interp_sort ?loc evd = function - | GProp -> evd, Prop Null - | GSet -> evd, Prop Pos - | GType n -> - let evd, u = interp_universe ?loc evd n in - evd, Type u - -let interp_elimination_sort = function - | GProp -> InProp - | GSet -> InSet - | GType _ -> InType - type inference_hook = env -> evar_map -> evar -> evar_map * constr type inference_flags = { diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7395e94a09..5822f5add5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,7 +18,6 @@ open Evd open EConstr open Glob_term open Evarutil -open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) @@ -119,9 +118,6 @@ val ise_pretype_gen : (** To embed constr in glob_constr *) -val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts -val interp_elimination_sort : glob_sort -> sorts_family - val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4a103cdd23..37204c2134 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -380,9 +380,9 @@ let tag_var = tag Tag.variable match bl with | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl - | _ -> assert false + | [] -> assert false let pr_binders_gen pr_c sep is_open = if is_open then pr_delimited_binders pr_com_at sep pr_c diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4c50c2f368..fa2b166dae 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -275,7 +275,7 @@ open Decl_kinds ) ++ hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s) + hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) | CaseScheme (dep,ind,s) -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() @@ -283,7 +283,7 @@ open Decl_kinds ) ++ hov 0 ((if dep then keyword "Elimination for" else keyword "Case for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s) + hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 9c58df5b21..31ede2d8b7 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,7 +10,7 @@ open CErrors open Pp open Util -let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp +let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () diff --git a/tactics/leminv.ml b/tactics/leminv.ml index aeb80ae57c..967ec2a71b 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -248,9 +248,9 @@ let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () in let evd = ref (Evd.from_env env) in let c = Constrintern.interp_type_evars env evd com in - let sigma, sort = Pretyping.interp_sort !evd comsort in + let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in try - add_inversion_lemma na env sigma c sort bool tac + add_inversion_lemma na env evd c sort bool tac with | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) user_err ~hdr:"Inv needs Nodep Prop Set" s diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 41b0e09b42..8745ad3979 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -15,5 +15,5 @@ val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) -> + Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bc55d3fe..32e366bc44 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4131,7 +4131,7 @@ let guess_elim isrec dep s hyp0 gl = let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in - if use_dependent_propositions_elimination () && dep + if use_dependent_propositions_elimination () && dep = Some true then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in @@ -4165,7 +4165,7 @@ let find_induction_type isrec elim hyp0 gl = | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in let _, (elimc,elimt),_ = - guess_elim isrec (* dummy: *) true sort hyp0 gl in + guess_elim isrec None sort hyp0 gl in let scheme = compute_elim_sig sigma ~elimc elimt in (* We drop the scheme waiting to know if it is dependent *) scheme, ElimOver (isrec,hyp0) @@ -4199,7 +4199,7 @@ let get_eliminator elim dep s gl = | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> - let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in + let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in let _, (l, s) = compute_elim_signature elims id in let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) (List.rev s.branches) diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v index 405d09809c..7ecfd98b67 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/4623.v @@ -2,4 +2,4 @@ Goal Type -> Type. set (T := Type). clearbody T. refine (@id _). -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v index a737afcdab..f5ce981cd0 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/4624.v @@ -4,4 +4,4 @@ Canonical Structure fooA (T : Type) := mkfoo (T -> T). Definition id (t : foo) (x : type t) := x. -Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file +Definition bar := id _ ((fun x : nat => x) : _). diff --git a/test-suite/bugs/closed/1425.v b/test-suite/bugs/closed/1425.v index 6be30174ae..775d278e74 100644 --- a/test-suite/bugs/closed/1425.v +++ b/test-suite/bugs/closed/1425.v @@ -16,4 +16,4 @@ Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1. intro n. setoid_rewrite recursion_S. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/1738.v b/test-suite/bugs/closed/1738.v index c2926a2b25..ef52c876c1 100644 --- a/test-suite/bugs/closed/1738.v +++ b/test-suite/bugs/closed/1738.v @@ -27,4 +27,4 @@ Module Test (Import M:FSetInterface.S). rewrite H in H0. assumption. Qed. -End Test.
\ No newline at end of file +End Test. diff --git a/test-suite/bugs/closed/1900.v b/test-suite/bugs/closed/1900.v index cf03efda42..6eea5db083 100644 --- a/test-suite/bugs/closed/1900.v +++ b/test-suite/bugs/closed/1900.v @@ -5,4 +5,4 @@ Definition eq_A := @eq A. Goal forall x, eq_A x x. intros. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/1901.v b/test-suite/bugs/closed/1901.v index 7d86adbfb2..98e017f9d6 100644 --- a/test-suite/bugs/closed/1901.v +++ b/test-suite/bugs/closed/1901.v @@ -8,4 +8,4 @@ Record Poset{A:Type}(Le : relation A) : Type := Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. Definition nat_Poset : Poset Peano.le. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/1905.v b/test-suite/bugs/closed/1905.v index 8c81d7510b..3b8a3d2f68 100644 --- a/test-suite/bugs/closed/1905.v +++ b/test-suite/bugs/closed/1905.v @@ -10,4 +10,4 @@ Goal forall a s, Proof. intros a s Ia. rewrite InE in Ia. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/1915.v b/test-suite/bugs/closed/1915.v index 7e62437d7b..2b0aed8c7d 100644 --- a/test-suite/bugs/closed/1915.v +++ b/test-suite/bugs/closed/1915.v @@ -3,4 +3,4 @@ Require Import Setoid. Fail Goal forall x, impl True (x = 0) -> x = 0 -> False. (*intros x H E. -rewrite H in E.*)
\ No newline at end of file +rewrite H in E.*) diff --git a/test-suite/bugs/closed/1939.v b/test-suite/bugs/closed/1939.v index 5e61529b4b..7b430ace5e 100644 --- a/test-suite/bugs/closed/1939.v +++ b/test-suite/bugs/closed/1939.v @@ -16,4 +16,4 @@ Require Import Setoid Program.Basics. intros x y H1 H2. rewrite H1. auto. - Qed.
\ No newline at end of file + Qed. diff --git a/test-suite/bugs/closed/1962.v b/test-suite/bugs/closed/1962.v index a6b0fee584..37b0dde06d 100644 --- a/test-suite/bugs/closed/1962.v +++ b/test-suite/bugs/closed/1962.v @@ -52,4 +52,4 @@ unfold triple, couple. Time fsetdec. Qed. -End BuildFSets.
\ No newline at end of file +End BuildFSets. diff --git a/test-suite/bugs/closed/2027.v b/test-suite/bugs/closed/2027.v index fb53c6ef43..ebc2bc070c 100644 --- a/test-suite/bugs/closed/2027.v +++ b/test-suite/bugs/closed/2027.v @@ -8,4 +8,4 @@ Goal forall A (p : T A), P p. Proof. intros. rewrite <- f_id. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/2136.v b/test-suite/bugs/closed/2136.v index d2b926f379..2fcfbe40dc 100644 --- a/test-suite/bugs/closed/2136.v +++ b/test-suite/bugs/closed/2136.v @@ -58,4 +58,4 @@ fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2137.v b/test-suite/bugs/closed/2137.v index 6c2023ab7b..b1f54b1766 100644 --- a/test-suite/bugs/closed/2137.v +++ b/test-suite/bugs/closed/2137.v @@ -49,4 +49,4 @@ fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v index c556ff0b2b..22e33c8e81 100644 --- a/test-suite/bugs/closed/2141.v +++ b/test-suite/bugs/closed/2141.v @@ -13,4 +13,4 @@ Module NatSet' := FSetHide NatSet. Recursive Extraction NatSet'.fold. Extraction TestCompile NatSet'.fold. -(* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file +(* Extraction "test2141.ml" NatSet'.fold. *) diff --git a/test-suite/bugs/closed/2281.v b/test-suite/bugs/closed/2281.v index 40948d9059..8f549b9201 100644 --- a/test-suite/bugs/closed/2281.v +++ b/test-suite/bugs/closed/2281.v @@ -47,4 +47,4 @@ intros. fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v index 7fae328715..14a3e5a7b0 100644 --- a/test-suite/bugs/closed/2310.v +++ b/test-suite/bugs/closed/2310.v @@ -18,4 +18,4 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. Unset Solve Unification Constraints. (* Keep the unification constraint around *) refine (Cons (cast H _ y)). intros. - refine (Nest (prod X X)). Qed.
\ No newline at end of file + refine (Nest (prod X X)). Qed. diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v index e06fb97590..73d95e91a1 100644 --- a/test-suite/bugs/closed/2319.v +++ b/test-suite/bugs/closed/2319.v @@ -10,4 +10,4 @@ Section S. with t : A unit := mkA unit (mkA unit t). Timeout 5 Eval vm_compute in s. -End S.
\ No newline at end of file +End S. diff --git a/test-suite/bugs/closed/2464.v b/test-suite/bugs/closed/2464.v index af70858720..b9db30359c 100644 --- a/test-suite/bugs/closed/2464.v +++ b/test-suite/bugs/closed/2464.v @@ -36,4 +36,4 @@ Lemma foo : forall (pu_type : Type) NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns). Proof. NameSetDec.fsetdec. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2473.v b/test-suite/bugs/closed/2473.v index fb676c7e47..0e7c0c25fa 100644 --- a/test-suite/bugs/closed/2473.v +++ b/test-suite/bugs/closed/2473.v @@ -37,4 +37,4 @@ Section S3. rewrite <- H. (* ok *) admit. Qed. -End S3.
\ No newline at end of file +End S3. diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v index a5f4ae64a0..ef2e4e3555 100644 --- a/test-suite/bugs/closed/2584.v +++ b/test-suite/bugs/closed/2584.v @@ -86,4 +86,4 @@ should be "Prop" or "Set". Elimination of an inductive object of sort Set is not allowed on a predicate in sort Type because strong elimination on non-small inductive types leads to paradoxes. -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/2586.v b/test-suite/bugs/closed/2586.v index 7e02e7f110..e57bcc25bb 100644 --- a/test-suite/bugs/closed/2586.v +++ b/test-suite/bugs/closed/2586.v @@ -3,4 +3,4 @@ Require Import Setoid SetoidClass Program. Goal forall `(Setoid nat) x y, x == y -> S x == S y. intros. Fail clsubst H0. - Abort.
\ No newline at end of file + Abort. diff --git a/test-suite/bugs/closed/2602.v b/test-suite/bugs/closed/2602.v index f074478868..29c8ac16b2 100644 --- a/test-suite/bugs/closed/2602.v +++ b/test-suite/bugs/closed/2602.v @@ -5,4 +5,4 @@ match goal with match goal with | |- S a > 0 => idtac end -end.
\ No newline at end of file +end. diff --git a/test-suite/bugs/closed/2615.v b/test-suite/bugs/closed/2615.v index 38c1cfc848..26c0f334d0 100644 --- a/test-suite/bugs/closed/2615.v +++ b/test-suite/bugs/closed/2615.v @@ -14,4 +14,4 @@ refine (fun p => match p with _ => _ end). Undo. refine (fun p => match p with foo_intro _ _ => _ end). admit. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2668.v b/test-suite/bugs/closed/2668.v index 74c8fa347b..d5bbfd3f08 100644 --- a/test-suite/bugs/closed/2668.v +++ b/test-suite/bugs/closed/2668.v @@ -3,4 +3,4 @@ Require Import MSetProperties. Module Pos := MSetPositive.PositiveSet. Module PPPP := MSetProperties.WPropertiesOn(Pos). -Print Module PPPP.
\ No newline at end of file +Print Module PPPP. diff --git a/test-suite/bugs/closed/2734.v b/test-suite/bugs/closed/2734.v index 826361be2b..3210214ea1 100644 --- a/test-suite/bugs/closed/2734.v +++ b/test-suite/bugs/closed/2734.v @@ -12,4 +12,4 @@ Inductive control := Go: expr -> control. Definition program := (Adr.t * (control))%type. -Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).
\ No newline at end of file +Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ). diff --git a/test-suite/bugs/closed/2750.v b/test-suite/bugs/closed/2750.v index fc580f1018..9d65e51f63 100644 --- a/test-suite/bugs/closed/2750.v +++ b/test-suite/bugs/closed/2750.v @@ -20,4 +20,4 @@ Module Test_ModWithRecord (M : ModWithRecord). {| M.A := 0 ; M.B := 2 |}. -End Test_ModWithRecord.
\ No newline at end of file +End Test_ModWithRecord. diff --git a/test-suite/bugs/closed/2837.v b/test-suite/bugs/closed/2837.v index 5d98446395..52a56c2cff 100644 --- a/test-suite/bugs/closed/2837.v +++ b/test-suite/bugs/closed/2837.v @@ -12,4 +12,4 @@ Fail rewrite test. Fail (intros; rewrite test). (* III) a working variant: *) -intros; rewrite (test n m).
\ No newline at end of file +intros; rewrite (test n m). diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v index 828e3b8c1f..e234630332 100644 --- a/test-suite/bugs/closed/2848.v +++ b/test-suite/bugs/closed/2848.v @@ -7,4 +7,4 @@ Add Parametric Relation : _ equiv' reflexivity proved by (Equivalence.equiv_reflexive cheat) transitivity proved by (Equivalence.equiv_transitive cheat) as apply_equiv'_rel. -Check apply_equiv'_rel : PreOrder equiv'.
\ No newline at end of file +Check apply_equiv'_rel : PreOrder equiv'. diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v index 45e24b5f5c..11fd7bada7 100644 --- a/test-suite/bugs/closed/2955.v +++ b/test-suite/bugs/closed/2955.v @@ -49,4 +49,4 @@ Module E. assumption. Qed. -End E.
\ No newline at end of file +End E. diff --git a/test-suite/bugs/closed/2983.v b/test-suite/bugs/closed/2983.v index 15598352b1..ad76350949 100644 --- a/test-suite/bugs/closed/2983.v +++ b/test-suite/bugs/closed/2983.v @@ -5,4 +5,4 @@ End ModB. Module Foo(A : ModA)(B : ModB A). End Foo. -Print Module Foo.
\ No newline at end of file +Print Module Foo. diff --git a/test-suite/bugs/closed/2995.v b/test-suite/bugs/closed/2995.v index ba3acd088d..b6c5b6df44 100644 --- a/test-suite/bugs/closed/2995.v +++ b/test-suite/bugs/closed/2995.v @@ -6,4 +6,4 @@ Module Implementation <: Interface. Definition t := bool. Definition error: t := false. Fail End Implementation. -(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file +(* A UserError here is expected, not an uncaught Not_found *) diff --git a/test-suite/bugs/closed/3008.v b/test-suite/bugs/closed/3008.v index 3f3a979a35..1979eda820 100644 --- a/test-suite/bugs/closed/3008.v +++ b/test-suite/bugs/closed/3008.v @@ -26,4 +26,4 @@ Fail Module Toto (* NB : the Inductive above and the A=A weren't in the initial test, they are here only to force an access to the environment - (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file + (cf [Printer.qualid_of_global]) and check that this env is ok. *) diff --git a/test-suite/bugs/closed/3319.v b/test-suite/bugs/closed/3319.v index 3b37e39e52..fbf5d86dcb 100644 --- a/test-suite/bugs/closed/3319.v +++ b/test-suite/bugs/closed/3319.v @@ -23,4 +23,4 @@ Section precategory. = morphism' xa yb. Proof. admit. - Defined.
\ No newline at end of file + Defined. diff --git a/test-suite/bugs/closed/3331.v b/test-suite/bugs/closed/3331.v index 9cd44bd0ca..b7dbb290e1 100644 --- a/test-suite/bugs/closed/3331.v +++ b/test-suite/bugs/closed/3331.v @@ -28,4 +28,4 @@ Section groupoid_category. clear H' foo. Set Typeclasses Debug. pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index 555accfd51..bf2f7a9d19 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -32,4 +32,4 @@ simpl. Set Printing Universes. exact hprop_Empty. Defined. -End B.
\ No newline at end of file +End B. diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v index cb435e7865..1d9e783374 100644 --- a/test-suite/bugs/closed/3387.v +++ b/test-suite/bugs/closed/3387.v @@ -19,4 +19,4 @@ Proof. first [ unify x y | fail 2 "no unify" ]; change x with y at -1. (* Error: Not convertible. *) reflexivity. -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 3a59869546..a03db77544 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -37,4 +37,4 @@ Proof. rewrite eissect; apply apD ). -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/3402.v b/test-suite/bugs/closed/3402.v index ed47ec8255..b4705780db 100644 --- a/test-suite/bugs/closed/3402.v +++ b/test-suite/bugs/closed/3402.v @@ -4,4 +4,4 @@ Goal forall A B (p : prod A B), p = let (x, y) := p in pair A B x y. Proof. intros A B p. exact eq_refl. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3428.v b/test-suite/bugs/closed/3428.v index 3eb75e43ac..16ace90af3 100644 --- a/test-suite/bugs/closed/3428.v +++ b/test-suite/bugs/closed/3428.v @@ -32,4 +32,4 @@ z' : prod A B p : @paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z') q : @paths ?54 (foo.snd ?42 ?45 z) (foo.snd ?57 ?60 z') The term "p" has type "@paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z')" -while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *)
\ No newline at end of file +while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *) diff --git a/test-suite/bugs/closed/3439.v b/test-suite/bugs/closed/3439.v index 1ea24bf1b8..e8c2d8b8ca 100644 --- a/test-suite/bugs/closed/3439.v +++ b/test-suite/bugs/closed/3439.v @@ -41,4 +41,4 @@ Module prim. Undo. solve [ typeclasses eauto ]. (* Error: No applicable tactic. *) Defined. -End prim.
\ No newline at end of file +End prim. diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v index 50d2978077..ddfb339443 100644 --- a/test-suite/bugs/closed/3441.v +++ b/test-suite/bugs/closed/3441.v @@ -20,4 +20,4 @@ Timeout 1 let H := fresh "H" in Timeout 1 Time let H := fresh "H" in let x := constr:(let n := 17 in do_n n = do_n n) in let y := (eval lazy in x) in - assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file + assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index dce73e1a50..8a0c98c333 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -48,4 +48,4 @@ Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100. Admitted. Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := - path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file + path_sigma_uncurried P u v o pr1^-1. diff --git a/test-suite/bugs/closed/3477.v b/test-suite/bugs/closed/3477.v index e941486472..3ed63604ea 100644 --- a/test-suite/bugs/closed/3477.v +++ b/test-suite/bugs/closed/3477.v @@ -6,4 +6,4 @@ Proof. intros A B. evar (a : prod A B); evar (f : (prod A B -> Set)). let a' := (eval unfold a in a) in - set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))).
\ No newline at end of file + set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))). diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v index a81837e714..35e0c51a93 100644 --- a/test-suite/bugs/closed/3480.v +++ b/test-suite/bugs/closed/3480.v @@ -45,4 +45,4 @@ yb : object StrX x : xa <~=~> yb The term "morphism_isomorphic:@morphism (precategory_of_structures P) xa yb" has type "@morphism (precategory_of_structures P) xa yb" -while it is expected to have type "morphism ?40 ?41 ?42". *)
\ No newline at end of file +while it is expected to have type "morphism ?40 ?41 ?42". *) diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v index 34a5e73da7..87fd2723c9 100644 --- a/test-suite/bugs/closed/3482.v +++ b/test-suite/bugs/closed/3482.v @@ -8,4 +8,4 @@ Check foo _. (* Toplevel input, characters 6-11: Error: Illegal application (Non-functional construction): The expression "foo" of type "True" cannot be applied to the term - "?36" : "?35" *)
\ No newline at end of file + "?36" : "?35" *) diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v index dc88a332b4..a0e157303f 100644 --- a/test-suite/bugs/closed/3484.v +++ b/test-suite/bugs/closed/3484.v @@ -28,4 +28,4 @@ T : Type H : sigT T (fun g : T => paths g g) x : T Unable to unify "paths (@projT1 ?24 ?23 ?25) (@projT1 ?24 ?23 ?26)" with - "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *)
\ No newline at end of file + "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *) diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 9ed0926a66..5adc48215e 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -91,4 +91,4 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v index 764a7334e8..3502b4f549 100644 --- a/test-suite/bugs/closed/3531.v +++ b/test-suite/bugs/closed/3531.v @@ -51,4 +51,4 @@ Goal forall b, (exists e1 e2 e3, admit. admit. Show Universes. -Time Qed.
\ No newline at end of file +Time Qed. diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v index 65ce4fb6b0..a740675f30 100644 --- a/test-suite/bugs/closed/3560.v +++ b/test-suite/bugs/closed/3560.v @@ -12,4 +12,4 @@ Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C). Proof. intros. exists (fun u => fun x => u (fst x) (snd x)). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v index f6cbc92992..ef4422eeac 100644 --- a/test-suite/bugs/closed/3561.v +++ b/test-suite/bugs/closed/3561.v @@ -21,4 +21,4 @@ Goal forall (H0 H2 : Type) x p, intros. match goal with | [ |- context[x (?f _)] ] => set(foo':=f) - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/3567.v b/test-suite/bugs/closed/3567.v index cb16b3ae4a..00c9c05469 100644 --- a/test-suite/bugs/closed/3567.v +++ b/test-suite/bugs/closed/3567.v @@ -65,4 +65,4 @@ ap (path_prod_uncurried z0 z') which is ill-typed. Reason is: Pattern-matching expression on an object of inductive type prod has invalid information. - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v index 3d4660b487..37fe46376e 100644 --- a/test-suite/bugs/closed/3584.v +++ b/test-suite/bugs/closed/3584.v @@ -13,4 +13,4 @@ Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B)) | existT _ false b => inr b end. (* Toplevel input, characters 0-182: Error: Pattern-matching expression on an object of inductive type sigT -has invalid information. *)
\ No newline at end of file +has invalid information. *) diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v index 3ef9270d40..9fded85a8d 100644 --- a/test-suite/bugs/closed/3590.v +++ b/test-suite/bugs/closed/3590.v @@ -9,4 +9,4 @@ Qed. (* Toplevel input, characters 20-58: Error: Failed to get enough information from the left-hand side to type the -right-hand side. *)
\ No newline at end of file +right-hand side. *) diff --git a/test-suite/bugs/closed/3594.v b/test-suite/bugs/closed/3594.v index d1aae7b440..1f86f4bd70 100644 --- a/test-suite/bugs/closed/3594.v +++ b/test-suite/bugs/closed/3594.v @@ -48,4 +48,4 @@ while it is expected to have type object := opposite D; morphism := fun s d : opposite D => morphism (opposite D) d s |}" and "opposite D"). - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3596.v b/test-suite/bugs/closed/3596.v index 49dd7be5a8..1ee9a5d8c1 100644 --- a/test-suite/bugs/closed/3596.v +++ b/test-suite/bugs/closed/3596.v @@ -16,4 +16,4 @@ Goal forall f b, Bar b = Bar b -> Foo f = Foo f. Fail progress unfold Bar. (* success *) Fail progress unfold Foo. (* failed to progress *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3618.v b/test-suite/bugs/closed/3618.v index dc560ad525..674b4cc2f4 100644 --- a/test-suite/bugs/closed/3618.v +++ b/test-suite/bugs/closed/3618.v @@ -100,4 +100,4 @@ Hint Mode IsEquiv - - + : typeclass_instances. Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} (P Q : Type) {Q_inO : inO_internal Q} -: IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _.
\ No newline at end of file +: IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _. diff --git a/test-suite/bugs/closed/3624.v b/test-suite/bugs/closed/3624.v index a05d5eb215..024243cfd3 100644 --- a/test-suite/bugs/closed/3624.v +++ b/test-suite/bugs/closed/3624.v @@ -8,4 +8,4 @@ Module Prim. Set Primitive Projections. Class foo (m : Set) := { pf : m = m }. Notation pf' m := (pf (m:=m)). (* Wrong argument name: m. *) -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v index 6a952377ce..52bb307271 100644 --- a/test-suite/bugs/closed/3633.v +++ b/test-suite/bugs/closed/3633.v @@ -7,4 +7,4 @@ Proof. (* Ensure the constraints are solved independently, otherwise a frozen ?A makes a search for Contr ?A fail when finishing to apply (fun x => x) *) apply (fun x => x), center. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3638.v b/test-suite/bugs/closed/3638.v index 70144174d7..5441fbedce 100644 --- a/test-suite/bugs/closed/3638.v +++ b/test-suite/bugs/closed/3638.v @@ -22,4 +22,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B), (* Toplevel input, characters 15-114: -Anomaly: Bad recursive type. Please report. *)
\ No newline at end of file +Anomaly: Bad recursive type. Please report. *) diff --git a/test-suite/bugs/closed/3640.v b/test-suite/bugs/closed/3640.v index bdbfbb152b..5dff98ba23 100644 --- a/test-suite/bugs/closed/3640.v +++ b/test-suite/bugs/closed/3640.v @@ -28,4 +28,4 @@ Proof. simpl in *. Fail match type of H with | _ = negb ?T => unify T (f.1 true); fail 1 "still has f.1 true" - end. (* Error: Tactic failure: still has f.1 true. *)
\ No newline at end of file + end. (* Error: Tactic failure: still has f.1 true. *) diff --git a/test-suite/bugs/closed/3641.v b/test-suite/bugs/closed/3641.v index f47f64ead7..730ab3f431 100644 --- a/test-suite/bugs/closed/3641.v +++ b/test-suite/bugs/closed/3641.v @@ -18,4 +18,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B), match goal with | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in pose (e' := e) end. - Fail change ?g with e'. (* Stack overflow *)
\ No newline at end of file + Fail change ?g with e'. (* Stack overflow *) diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v index ba6006ed93..58aa161403 100644 --- a/test-suite/bugs/closed/3648.v +++ b/test-suite/bugs/closed/3648.v @@ -80,4 +80,4 @@ Error: Found no subterm matching "F _1 (identity (fst x))" in the current goal. *) rewrite identity_of. (* Toplevel input, characters 15-34: Error: -Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *)
\ No newline at end of file +Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *) diff --git a/test-suite/bugs/closed/3658.v b/test-suite/bugs/closed/3658.v index 622c3c94ac..74f4e82dbb 100644 --- a/test-suite/bugs/closed/3658.v +++ b/test-suite/bugs/closed/3658.v @@ -72,4 +72,4 @@ Module Prim. end. (* Error: Tactic failure: bad H1. *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3661.v b/test-suite/bugs/closed/3661.v index fdca49bc42..1f13ffcf34 100644 --- a/test-suite/bugs/closed/3661.v +++ b/test-suite/bugs/closed/3661.v @@ -85,4 +85,4 @@ Goal forall (x3 x9 : PreCategory) (x12 f0 : Functor x9 x3) (@morphism_inverse _ _ _ (@morphism_isomorphic (functor_category x9 x3) f0 x12 x35) _) x37) -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3664.v b/test-suite/bugs/closed/3664.v index 63a81b6d01..cd1427a143 100644 --- a/test-suite/bugs/closed/3664.v +++ b/test-suite/bugs/closed/3664.v @@ -21,4 +21,4 @@ Module Prim. Fail progress cbn. (* [cbn] succeeds incorrectly, giving [d x] *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v index e69ec10976..c7bc2f22a8 100644 --- a/test-suite/bugs/closed/3666.v +++ b/test-suite/bugs/closed/3666.v @@ -48,4 +48,4 @@ H' : H_f a (h c) = H_g b (h c) Unable to unify "hproptype (H_f a (h c))" with "?T (H_f a (h c))". *) Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3668.v b/test-suite/bugs/closed/3668.v index da01ed00e4..1add3dba1e 100644 --- a/test-suite/bugs/closed/3668.v +++ b/test-suite/bugs/closed/3668.v @@ -51,4 +51,4 @@ Module Prim. end. (* Tactic failure: bad *) all:admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3672.v b/test-suite/bugs/closed/3672.v index 283be49587..b355e7e9db 100644 --- a/test-suite/bugs/closed/3672.v +++ b/test-suite/bugs/closed/3672.v @@ -24,4 +24,4 @@ Record Ar3 C (A:AT) := ; id3 : forall X, ar3 X X }. (* The command has indeed failed with message: => Anomaly: Bad recursive type. Please report. -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v index 31de8ec45b..3882eee97c 100644 --- a/test-suite/bugs/closed/3698.v +++ b/test-suite/bugs/closed/3698.v @@ -23,4 +23,4 @@ Proof. assert (H'' : forall g : X = Y -> (issig_hSet^-1 X).1 = (issig_hSet^-1 Y).1, g = g -> IsEquiv g) by admit. Eval compute in (@projT1 Type IsHSet (@equiv_inv _ _ _ (equiv_isequiv _ _ issig_hSet) X)). - Fail apply H''. (* stack overflow *)
\ No newline at end of file + Fail apply H''. (* stack overflow *) diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index efa4325264..dbb10f94f2 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -156,4 +156,4 @@ Module Prim. | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ]. admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3700.v b/test-suite/bugs/closed/3700.v index 4e226524cb..bac443e337 100644 --- a/test-suite/bugs/closed/3700.v +++ b/test-suite/bugs/closed/3700.v @@ -81,4 +81,4 @@ Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a /\ and (@eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x)) (@eq Set (@Prim.snd Set Set x) (@Prim.snd Set Set x))) *) Unset Printing All. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v index 7282500769..feeb04d64e 100644 --- a/test-suite/bugs/closed/3703.v +++ b/test-suite/bugs/closed/3703.v @@ -29,4 +29,4 @@ Module Keyed. rewrite <- H'. admit. Defined. -End Keyed.
\ No newline at end of file +End Keyed. diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 76beedf687..09f1149c20 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -102,4 +102,4 @@ cannot be applied to the terms "G0" : "list Type" The 2nd term has type "Type@{Top.53}" which should be coercible to "Type@{Top.12}". - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v index a50572ace0..aced9615ee 100644 --- a/test-suite/bugs/closed/3735.v +++ b/test-suite/bugs/closed/3735.v @@ -1,4 +1,4 @@ Require Import Coq.Program.Tactics. Class Foo := { bar : Type }. Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *) -Fail Program Lemma foo : Foo -> bar.
\ No newline at end of file +Fail Program Lemma foo : Foo -> bar. diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index c799d4393f..ca78987bf3 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -8,4 +8,4 @@ Add Parametric Relation A transitivity proved by transitivity as refine_rel. (* Toplevel input, characters 20-118: -Anomaly: index to an anonymous variable. Please report. *)
\ No newline at end of file +Anomaly: index to an anonymous variable. Please report. *) diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v index 5bfbee9494..f586438cdd 100644 --- a/test-suite/bugs/closed/3753.v +++ b/test-suite/bugs/closed/3753.v @@ -1,4 +1,4 @@ Axiom foo : Type -> Type. Axiom bar : forall (T : Type), T -> foo T. Arguments bar A x : rename. -About bar.
\ No newline at end of file +About bar. diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v index 2dc50c17d0..16b0b8b603 100644 --- a/test-suite/bugs/closed/3782.v +++ b/test-suite/bugs/closed/3782.v @@ -61,4 +61,4 @@ The term "e'" has type "@IsEquiv md mc e" while it is expected to have type *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v index e217129688..f7e2b54353 100644 --- a/test-suite/bugs/closed/3783.v +++ b/test-suite/bugs/closed/3783.v @@ -30,4 +30,4 @@ Module Prim. Timeout 1 cbv beta in y. (* takes around 2s. Grows with the value passed to [exp] above *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v index 108ebf592b..a6286f0377 100644 --- a/test-suite/bugs/closed/3807.v +++ b/test-suite/bugs/closed/3807.v @@ -30,4 +30,4 @@ Axiom f@{i} : Type@{i}. (* *** [ f@{i} : Type@{i} ] (* i |= *) -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v index a5c84e6856..ac6a850193 100644 --- a/test-suite/bugs/closed/3808.v +++ b/test-suite/bugs/closed/3808.v @@ -1,3 +1,3 @@ Unset Strict Universe Declaration. Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) - := foo : Foo.
\ No newline at end of file + := foo : Foo. diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v index 355d23a58b..0b9c3183cc 100644 --- a/test-suite/bugs/closed/3819.v +++ b/test-suite/bugs/closed/3819.v @@ -6,4 +6,4 @@ Lemma test1 (X:Type) : eq (op OpType X) X. Proof eq_refl. Definition test2 (A:Type) : eq (op _ A) A. -Proof eq_refl.
\ No newline at end of file +Proof eq_refl. diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index bb6af6a66c..7c60ddf347 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -32,4 +32,4 @@ Proof. apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ (fun b => ap g (eisretr f b))). Qed. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v index 2ac4abe54f..b523b117e5 100644 --- a/test-suite/bugs/closed/3886.v +++ b/test-suite/bugs/closed/3886.v @@ -20,4 +20,4 @@ Obligation 1 of doubleO. apply cheat. Qed. -Check doubleE.
\ No newline at end of file +Check doubleE. diff --git a/test-suite/bugs/closed/3899.v b/test-suite/bugs/closed/3899.v index e83166aaec..7754934c0b 100644 --- a/test-suite/bugs/closed/3899.v +++ b/test-suite/bugs/closed/3899.v @@ -8,4 +8,4 @@ Fail Check fun x y : unit => eq_refl : x = y. Record ok : Set := tt' { a : unit }. Record nonprim : Prop := { undef : unit }. -Record prim : Prop := { def : True }.
\ No newline at end of file +Record prim : Prop := { def : True }. diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v index 5e5ba816f9..ac9c50369b 100644 --- a/test-suite/bugs/closed/3943.v +++ b/test-suite/bugs/closed/3943.v @@ -47,4 +47,4 @@ Definition path_isomorphic (i j : Isomorphic s d) Admitted. Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q -: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file +: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q. diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v index 66dee702aa..4957cc740d 100644 --- a/test-suite/bugs/closed/3956.v +++ b/test-suite/bugs/closed/3956.v @@ -140,4 +140,4 @@ Module Comodality_Theory (F : Comodality). End cip_FPHM. End isequiv_F_prod_cmp_M. -End Comodality_Theory.
\ No newline at end of file +End Comodality_Theory. diff --git a/test-suite/bugs/closed/3960.v b/test-suite/bugs/closed/3960.v index e56dcef74f..3527312486 100644 --- a/test-suite/bugs/closed/3960.v +++ b/test-suite/bugs/closed/3960.v @@ -23,4 +23,4 @@ Class myClassP (A : Type) := Instance myInstanceP : myClassP nat := { barP := fooP - }.
\ No newline at end of file + }. diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v index b6be159595..3d9e06b612 100644 --- a/test-suite/bugs/closed/3974.v +++ b/test-suite/bugs/closed/3974.v @@ -4,4 +4,4 @@ End S. Module Type M (X : S). Fail Module P (X : S). (* Used to say: Anomaly: X already exists. Please report. *) - (* Should rather say now: Error: X already exists. *)
\ No newline at end of file + (* Should rather say now: Error: X already exists. *) diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v index 95851c8137..c7616b3ab6 100644 --- a/test-suite/bugs/closed/3975.v +++ b/test-suite/bugs/closed/3975.v @@ -5,4 +5,4 @@ Module M (X:S). End M. Module Type P (X : S). Print M. (* Used to say: Anomaly: X already exists. Please report. *) - (* Should rather : print something :-) *)
\ No newline at end of file + (* Should rather : print something :-) *) diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v index ced13839dd..e17550e904 100644 --- a/test-suite/bugs/closed/3998.v +++ b/test-suite/bugs/closed/3998.v @@ -21,4 +21,4 @@ Axiom ex : RecordOf _ I1FieldType. Definition works := (fun ex' => update ex' C true) (update ex C false). Set Typeclasses Debug. -Definition doesnt := update (update ex C false) C true.
\ No newline at end of file +Definition doesnt := update (update ex C false) C true. diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v index 2b8641ebb0..6c23baffa0 100644 --- a/test-suite/bugs/closed/4031.v +++ b/test-suite/bugs/closed/4031.v @@ -11,4 +11,4 @@ Proof. change mytt with (@something _ mytt) in x. subst x. (* Proof works if this line is removed *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 61527764e2..606c6e0845 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -101,4 +101,4 @@ Variable T : Type. Goal @eq Type T T. congruence. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index ffd33d3813..8d7dfbd49b 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -84,4 +84,4 @@ O1 : T -> PointedOPred tr : T -> T O2 : PointedOPred x0 : T -H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v index 02aa25e09f..183b860d1f 100644 --- a/test-suite/bugs/closed/4097.v +++ b/test-suite/bugs/closed/4097.v @@ -62,4 +62,4 @@ Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2) : p = q - := path_path_sigma_uncurried P u v p q (r; s).
\ No newline at end of file + := path_path_sigma_uncurried P u v p q (r; s). diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v index a38b050966..75a26a0670 100644 --- a/test-suite/bugs/closed/4101.v +++ b/test-suite/bugs/closed/4101.v @@ -16,4 +16,4 @@ Lemma sigT_obj_eq Proof. intros. Set Debug Tactic Unification. - apply path_forall.
\ No newline at end of file + apply path_forall. diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v index 00db8f7f3c..315dc0d242 100644 --- a/test-suite/bugs/closed/4120.v +++ b/test-suite/bugs/closed/4120.v @@ -2,4 +2,4 @@ Definition id {T} (x : T) := x. Goal sigT (fun x => id x)%type. change (fun x => ?f x) with f. exists Type. exact Set. -Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file +Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *) diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v index fec64555f4..fc0b58cfe1 100644 --- a/test-suite/bugs/closed/4151.v +++ b/test-suite/bugs/closed/4151.v @@ -400,4 +400,4 @@ Section sound. Undo. assumption. Undo. - eassumption. (* no applicable tactic *)
\ No newline at end of file + eassumption. (* no applicable tactic *) diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v index aa2b189b67..d2003ab1f0 100644 --- a/test-suite/bugs/closed/4161.v +++ b/test-suite/bugs/closed/4161.v @@ -24,4 +24,4 @@ Inductive t : Type -> Type := Fixpoint test {A : Type} (x : t A) : t (A + unit) := match x in t A with | Just B x => @test B x - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v index 076a3c3d68..eb6867a033 100644 --- a/test-suite/bugs/closed/4203.v +++ b/test-suite/bugs/closed/4203.v @@ -16,4 +16,4 @@ Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok. Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok. Check (eq_refl t : t = t'). -Check (eq_refl t : t = t'').
\ No newline at end of file +Check (eq_refl t : t = t''). diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v index d684e8cf4b..2e620fce2a 100644 --- a/test-suite/bugs/closed/4214.v +++ b/test-suite/bugs/closed/4214.v @@ -3,4 +3,4 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v index 74cacf559a..f5d0d1a523 100644 --- a/test-suite/bugs/closed/4250.v +++ b/test-suite/bugs/closed/4250.v @@ -8,4 +8,4 @@ Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n. (* fails with "The reference A was not found in the current environment." *) Function f3 `{n:nat , u:Vector.t A n} := u. -Check R_f3_complete.
\ No newline at end of file +Check R_f3_complete. diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v index 66343d6671..f112e7b4d5 100644 --- a/test-suite/bugs/closed/4251.v +++ b/test-suite/bugs/closed/4251.v @@ -14,4 +14,4 @@ Check array Type. Check fun A : Type => Ref A. Definition abs_val (a : Type) := - bind (ref a) (fun r : array Type => array_make tt).
\ No newline at end of file + bind (ref a) (fun r : array Type => array_make tt). diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v index 591ea4b5b2..401e86649b 100644 --- a/test-suite/bugs/closed/4273.v +++ b/test-suite/bugs/closed/4273.v @@ -6,4 +6,4 @@ Theorem onefiber' (q : total2 (fun y => y = 0)) : True. Proof. assert (foo:=pr2 _ q). simpl in foo. destruct foo. (* Error: q is used in conclusion. *) exact I. Qed. -Print onefiber'.
\ No newline at end of file +Print onefiber'. diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v index ba82e6c376..ea9cbb210f 100644 --- a/test-suite/bugs/closed/4276.v +++ b/test-suite/bugs/closed/4276.v @@ -8,4 +8,4 @@ Definition bad' : True := mybox.(unwrap _ _). Fail Definition bad : False := unwrap _ _ mybox. -(* Closed under the global context *)
\ No newline at end of file +(* Closed under the global context *) diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index 43c9b51295..757b71b2dd 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -120,4 +120,4 @@ Definition setle (B : Type@{i}) := Fail Check @setlt@{j Prop}. Fail Definition foo := @setle@{j Prop}. Check setlt@{Set i}. -Check setlt@{Set j}.
\ No newline at end of file +Check setlt@{Set j}. diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v index 3671c931b7..21d333fa63 100644 --- a/test-suite/bugs/closed/4293.v +++ b/test-suite/bugs/closed/4293.v @@ -4,4 +4,4 @@ End Foo. Module M : Foo. Definition T := let X := Type in Type. -End M.
\ No newline at end of file +End M. diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v index 955c3017d7..a1daa193ae 100644 --- a/test-suite/bugs/closed/4299.v +++ b/test-suite/bugs/closed/4299.v @@ -9,4 +9,4 @@ End Foo. Module M : Foo with Definition U := Type : Type. Definition U := let X := Type in Type. Definition eq : Type = U := eq_refl. -Fail End M.
\ No newline at end of file +Fail End M. diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v index 4aef5bb95e..28f028ad89 100644 --- a/test-suite/bugs/closed/4306.v +++ b/test-suite/bugs/closed/4306.v @@ -29,4 +29,4 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) | Eq => x :: foo (xs', ys') | Gt => y :: foo (xs, ys') end - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v index 8e1bb31007..b40b3a4830 100644 --- a/test-suite/bugs/closed/4328.v +++ b/test-suite/bugs/closed/4328.v @@ -3,4 +3,4 @@ Axiom pi : forall (P : Prop) (p : P), Prop. Definition test1 A (x : _) := pi A x. (* success *) Fail Definition test2 A (x : A) := pi A x. (* failure ??? *) Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure *) -Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file +Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *) diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v index e71ddaf71f..c55b4cf02a 100644 --- a/test-suite/bugs/closed/4354.v +++ b/test-suite/bugs/closed/4354.v @@ -8,4 +8,4 @@ Proof. auto using closed_increment. Show Universes. Qed. (* also fails with -nois, so the content of the hint database does not matter -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v index 71e3a75187..468bade1cc 100644 --- a/test-suite/bugs/closed/4375.v +++ b/test-suite/bugs/closed/4375.v @@ -104,4 +104,4 @@ with cb@{i} (t : Type@{i}) : foo@{i} t := Print ca. Print cb. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v index 3189685ec0..62b90b4286 100644 --- a/test-suite/bugs/closed/4416.v +++ b/test-suite/bugs/closed/4416.v @@ -1,4 +1,4 @@ Goal exists x, x. Unset Solve Unification Constraints. unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. -(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file +(* Error: Incorrect number of goals (expected 2 tactics). *) diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v index 9eeb864689..83c0e3f81f 100644 --- a/test-suite/bugs/closed/4433.v +++ b/test-suite/bugs/closed/4433.v @@ -26,4 +26,4 @@ Proof. case proof_admitted. Unshelve. all:constructor. -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v index 66dfa0e685..a3a8717d98 100644 --- a/test-suite/bugs/closed/4443.v +++ b/test-suite/bugs/closed/4443.v @@ -28,4 +28,4 @@ Defined. Set Printing Universes. Check PROD@{i i i}. Check PRODinj@{i j}. -Fail Check PRODinj@{j i}.
\ No newline at end of file +Fail Check PRODinj@{j i}. diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v index ecebaba812..c1fe44315a 100644 --- a/test-suite/bugs/closed/4450.v +++ b/test-suite/bugs/closed/4450.v @@ -55,4 +55,4 @@ Proof. eauto using foo. Show Universes. Undo. eauto using foop. Show Proof. Show Universes. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v index 08a86330f2..98c05ee1a8 100644 --- a/test-suite/bugs/closed/4480.v +++ b/test-suite/bugs/closed/4480.v @@ -9,4 +9,4 @@ Admitted. Goal True. Fail setoid_rewrite foo. Fail setoid_rewrite trueI. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v index ccdb2dddda..379e46b3e3 100644 --- a/test-suite/bugs/closed/4498.v +++ b/test-suite/bugs/closed/4498.v @@ -21,4 +21,4 @@ Require Export Coq.Setoids.Setoid. Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with signature equiv ==> equiv ==> equiv as compose_mor. -Proof. apply comp_respects. Qed.
\ No newline at end of file +Proof. apply comp_respects. Qed. diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v index f54d6433d8..5162f352df 100644 --- a/test-suite/bugs/closed/4503.v +++ b/test-suite/bugs/closed/4503.v @@ -34,4 +34,4 @@ Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. -End Embed_ILogic_Pre.
\ No newline at end of file +End Embed_ILogic_Pre. diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v index ccbc47d20f..945183fae7 100644 --- a/test-suite/bugs/closed/4519.v +++ b/test-suite/bugs/closed/4519.v @@ -18,4 +18,4 @@ Check qux nat nat nat : Set. Check qux nat nat Set : Set. (* Error: The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is expected to have type "Set" -(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *) diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v index e7567623a6..2c90044dc7 100644 --- a/test-suite/bugs/closed/4603.v +++ b/test-suite/bugs/closed/4603.v @@ -7,4 +7,4 @@ Abort. Goal True. Definition foo (A : Type) : Prop:= True. set (x:=foo). split. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v index e1206bb37a..4f56e19584 100644 --- a/test-suite/bugs/closed/4627.v +++ b/test-suite/bugs/closed/4627.v @@ -46,4 +46,4 @@ The term "predicate nat (Build_sa nat)" has type while it is expected to have type "Type@{Top.208}" (universe inconsistency: Cannot enforce Top.205 <= Top.208 because Top.208 < Top.205). -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v index c94fa31a9d..3f41c5d6b1 100644 --- a/test-suite/bugs/closed/4679.v +++ b/test-suite/bugs/closed/4679.v @@ -15,4 +15,4 @@ Proof. Undo. setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v index 8884812102..5fb9696f3f 100644 --- a/test-suite/bugs/closed/4723.v +++ b/test-suite/bugs/closed/4723.v @@ -25,4 +25,4 @@ Program Fact kp_assoc (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): kp x (kp y z) = kp (kp x y) z. admit. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v index 5bb3cd1be7..67d645a68f 100644 --- a/test-suite/bugs/closed/4754.v +++ b/test-suite/bugs/closed/4754.v @@ -32,4 +32,4 @@ Proof. pose proof (_ : (Proper (_ ==> eq ==> _) and)). setoid_rewrite (FG _ _); [ | reflexivity.. ]. Undo. - setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted. diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v index ae8ed0e6e8..9613b5c248 100644 --- a/test-suite/bugs/closed/4763.v +++ b/test-suite/bugs/closed/4763.v @@ -10,4 +10,4 @@ Goal forall x y z, leb x y -> leb y z -> True. => pose proof (transitivity H H' : is_true (R x z)) end. exact I. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v index 33a1d1a50b..f0c91f7b49 100644 --- a/test-suite/bugs/closed/4769.v +++ b/test-suite/bugs/closed/4769.v @@ -91,4 +91,4 @@ Section Adjunction. (oppositeC C) D C (identityF (oppositeC C)) G)) }. -End Adjunction.
\ No newline at end of file +End Adjunction. diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v index 6d21b66fe9..ac5d7ea287 100644 --- a/test-suite/bugs/closed/4869.v +++ b/test-suite/bugs/closed/4869.v @@ -15,4 +15,4 @@ Section Foo. Constraint Set < j. Definition foo := Type@{j}. -End Foo.
\ No newline at end of file +End Foo. diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index f2f917b4e7..3be36d8475 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -69,4 +69,4 @@ Proof. destruct xs; simpl; intros; subst; auto. generalize dependent t. simpl in *. induction xs; simpl in *; intros; congruence. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v index 7e3c78dc2e..7d153d9828 100644 --- a/test-suite/bugs/closed/4877.v +++ b/test-suite/bugs/closed/4877.v @@ -9,4 +9,4 @@ Ltac induction_last := Goal forall n m : nat, True -> n = m -> m = n. induction_last. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v index 12c958be67..83f1677455 100644 --- a/test-suite/bugs/closed/5036.v +++ b/test-suite/bugs/closed/5036.v @@ -7,4 +7,4 @@ Section foo. autorewrite with core. constructor. Qed. -End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *) diff --git a/test-suite/bugs/closed/5065.v b/test-suite/bugs/closed/5065.v index 6bd677ba6f..932fee8b3b 100644 --- a/test-suite/bugs/closed/5065.v +++ b/test-suite/bugs/closed/5065.v @@ -3,4 +3,4 @@ Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar. Lemma L1 : foo -> True with L2 : bar -> True. intros; clear L1 L2; abstract (exact I). intros; exact I. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v index bcde510ee6..17231bffcf 100644 --- a/test-suite/bugs/closed/5123.v +++ b/test-suite/bugs/closed/5123.v @@ -30,4 +30,4 @@ Goal True. all:cycle 3. eapply existT. (*This does no typeclass resultion, which is correct.*) Focus 5. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v index 261092ee6d..05603a048c 100644 --- a/test-suite/bugs/closed/5180.v +++ b/test-suite/bugs/closed/5180.v @@ -61,4 +61,4 @@ The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). *) all:compute in *. - all:exact x.
\ No newline at end of file + all:exact x. diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v index ed137395fc..3428e1a450 100644 --- a/test-suite/bugs/closed/5203.v +++ b/test-suite/bugs/closed/5203.v @@ -2,4 +2,4 @@ Goal True. Typeclasses eauto := debug. Fail solve [ typeclasses eauto ]. Fail typeclasses eauto. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v index f1f1b8c051..d8824bff87 100644 --- a/test-suite/bugs/closed/5315.v +++ b/test-suite/bugs/closed/5315.v @@ -7,4 +7,4 @@ Function dumb_nope (a:nat) {struct a} := match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end. (* This check is just present to ensure Function worked well *) -Check R_dumb_nope_complete.
\ No newline at end of file +Check R_dumb_nope_complete. diff --git a/test-suite/bugs/closed/5434.v b/test-suite/bugs/closed/5434.v new file mode 100644 index 0000000000..5d2460face --- /dev/null +++ b/test-suite/bugs/closed/5434.v @@ -0,0 +1,18 @@ +(* About binders which remain unnamed after typing *) + +Global Set Asymmetric Patterns. + +Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : +@sig A P) : @sig A Q + := let 'exist a p := x in exist Q a (f a p). +Axioms (feBW' : Type) (g : Prop -> Prop) (f' : feBW' -> Prop). +Definition foo := @proj2_sig_map feBW' (fun H => True = f' _) (fun H => + g True = g (f' H)) + (fun (a : feBW') (p : (fun H : feBW' => True = + f' H) a) => @f_equal Prop Prop g True (f' a) p). +Print foo. +Goal True. + lazymatch type of foo with + | sig (fun a : ?A => ?P) -> _ + => pose (fun a : A => a = a /\ P = P) + end. diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v index 5bcdaa2f18..b9f0bc45c6 100644 --- a/test-suite/bugs/closed/5578.v +++ b/test-suite/bugs/closed/5578.v @@ -54,4 +54,4 @@ Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) f eta ( (Bind (k eta) (fun rands => ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). - (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *) diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v index ab88a88f44..47e0e92d2a 100644 --- a/test-suite/bugs/closed/5618.v +++ b/test-suite/bugs/closed/5618.v @@ -6,4 +6,4 @@ Function test {T} (v : T) (x : nat) : nat := | S x' => test v x' end. -Check R_test_complete.
\ No newline at end of file +Check R_test_complete. diff --git a/test-suite/bugs/closed/5707.v b/test-suite/bugs/closed/5707.v new file mode 100644 index 0000000000..785844c66d --- /dev/null +++ b/test-suite/bugs/closed/5707.v @@ -0,0 +1,12 @@ +(* Destruct and primitive projections *) + +(* Checking the (superficial) part of #5707: + "destruct" should be able to use non-dependent case analysis when + dependent case analysis is not available and unneeded *) + +Set Primitive Projections. + +Inductive foo := Foo { proj1 : nat; proj2 : nat }. + +Goal forall x : foo, True. +Proof. intros x. destruct x. diff --git a/test-suite/bugs/closed/5713.v b/test-suite/bugs/closed/5713.v new file mode 100644 index 0000000000..9daf9647fc --- /dev/null +++ b/test-suite/bugs/closed/5713.v @@ -0,0 +1,15 @@ +(* Checking that classical_right/classical_left work in an empty context *) + +Require Import Classical. + +Parameter A:Prop. + +Goal A \/ ~A. +classical_right. +assumption. +Qed. + +Goal ~A \/ A. +classical_left. +assumption. +Qed. diff --git a/test-suite/bugs/closed/808_2411.v b/test-suite/bugs/closed/808_2411.v index 1c13e74547..1169b2036b 100644 --- a/test-suite/bugs/closed/808_2411.v +++ b/test-suite/bugs/closed/808_2411.v @@ -24,4 +24,4 @@ rewrite bar'. now apply le_S. Qed. -End test.
\ No newline at end of file +End test. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index 223a98de1c..5c45036643 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -199,4 +199,4 @@ Fail Admitted. Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) : Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*) Proof. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v index 6b07c30404..a9e0bd2676 100644 --- a/test-suite/bugs/closed/HoTT_coq_080.v +++ b/test-suite/bugs/closed/HoTT_coq_080.v @@ -24,4 +24,4 @@ Goal forall C D (x y : ob (sum_category C D)), Type. intros C D x y. hnf in x, y. exact (hom (sum_category _ _) x y). -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 7c5dc41679..0b576db6b3 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -258,4 +258,4 @@ n). apply SynInc;apply H.mem_2;trivial. rewrite H in H0. discriminate. (* !! impossible here !! *) Qed. -End B.
\ No newline at end of file +End B. diff --git a/test-suite/bugs/opened/1811.v b/test-suite/bugs/opened/1811.v index 10c988fc02..57c1744313 100644 --- a/test-suite/bugs/opened/1811.v +++ b/test-suite/bugs/opened/1811.v @@ -7,4 +7,4 @@ Goal forall b1 b2, (negb b1 = b2) -> xorb true b1 = b2. Proof. intros b1 b2. Fail rewrite neg2xor. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v index 99ca6cb39d..e4711a38c0 100644 --- a/test-suite/bugs/opened/3794.v +++ b/test-suite/bugs/opened/3794.v @@ -4,4 +4,4 @@ Hint Unfold not : core. Goal true<>false. Set Typeclasses Debug. Fail typeclasses eauto with core. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v index 165813084d..5c4b4277b2 100644 --- a/test-suite/bugs/opened/3948.v +++ b/test-suite/bugs/opened/3948.v @@ -22,4 +22,4 @@ Module DepMap : Interface. let _ := @Dom.fold in tt. End DepMap. -Print Assumptions DepMap.constant.
\ No newline at end of file +Print Assumptions DepMap.constant. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index 7906a5b15e..d63a3548e5 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -64,4 +64,4 @@ I disable these tests because cqochk can't process them when compiled with (* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) -(* End subtyping_test. *)
\ No newline at end of file +(* End subtyping_test. *) diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v index ceccd4607d..9eb7e3bc20 100644 --- a/test-suite/failure/circular_subtyping.v +++ b/test-suite/failure/circular_subtyping.v @@ -7,4 +7,4 @@ Module NN <: T. Module M:=N. End NN. Fail Module P <: T with Module M:=NN := NN. Module F (X:S) (Y:T with Module M:=X). End F. -Fail Module G := F N N.
\ No newline at end of file +Fail Module G := F N N. diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v index cb39893f47..d193dc484f 100644 --- a/test-suite/failure/cofixpoint.v +++ b/test-suite/failure/cofixpoint.v @@ -12,4 +12,4 @@ Fail CoFixpoint loop : CoFalse := (cofix f := I with g := loop for g). Fail CoFixpoint loop : CoFalse := - (cofix f := loop with g := I for f).
\ No newline at end of file + (cofix f := loop with g := I for f). diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v index eda4a18673..3ae8770546 100644 --- a/test-suite/failure/guard-cofix.v +++ b/test-suite/failure/guard-cofix.v @@ -40,4 +40,4 @@ Fail CoFixpoint loop' : CoFalse := Omega match eq_sym H in _ = T return T with eq_refl => loop' end end. -Fail Definition ff' : False := match loop' with CF _ t => t end.
\ No newline at end of file +Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/sortelim.v b/test-suite/failure/sortelim.v index 2b3cf10660..3d2eef6a98 100644 --- a/test-suite/failure/sortelim.v +++ b/test-suite/failure/sortelim.v @@ -146,4 +146,4 @@ Qed. Print Assumptions pandora. -*)
\ No newline at end of file +*) diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v index 2ec7278080..d75620c257 100644 --- a/test-suite/ideal-features/implicit_binders.v +++ b/test-suite/ideal-features/implicit_binders.v @@ -121,4 +121,4 @@ Definition qux₁ {( F : `(SomeStruct a) )} : nat := 0. (** *** Questions - Autres propositions de syntaxe ? - Réactions sur la construction ? - *)
\ No newline at end of file + *) diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v index a96d4a5c7f..7fab2a58e8 100644 --- a/test-suite/interactive/ParalITP.v +++ b/test-suite/interactive/ParalITP.v @@ -44,4 +44,4 @@ split. exact a. Qed. -End Demo.
\ No newline at end of file +End Demo. diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v index 31e3493768..a865632e8c 100644 --- a/test-suite/interactive/proof_block.v +++ b/test-suite/interactive/proof_block.v @@ -63,4 +63,4 @@ split. split. split. - solve [ trivial ]. - solve [ trivial ]. - exact 6. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1f27fe1ba1..820fda172a 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -52,4 +52,4 @@ Print N'''.x. Import N'''. -Print t.
\ No newline at end of file +Print t. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index 57878a5f15..d2116d2183 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -16,4 +16,4 @@ Qed. Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m. eauto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 6198f29a0d..8ba8525c66 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -54,4 +54,4 @@ Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. info auto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 1d1b1e0ab2..ea49553942 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -27,4 +27,4 @@ Module List (X: ELEM). End List. -Module N := List Nat.
\ No newline at end of file +Module N := List Nat. diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index 9657c685d0..11ad205e40 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -12,4 +12,4 @@ Check (f 0 0). Check (f 0 0). Import M. Check (f 0 0). -Check (N.f 0 0).
\ No newline at end of file +Check (N.f 0 0). diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index d4ac7b3a24..8b5969dd76 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -31,4 +31,4 @@ Goal forall x, M.C x = M1.C 0 -> x = 0. par des modules differents *) inversion H. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 1238ee9deb..c8129eec5e 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -19,4 +19,4 @@ Module Z. Module N := M. End Z. -Module A : SIG := Z.
\ No newline at end of file +Module A : SIG := Z. diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v index f806a7c412..51f5f40078 100644 --- a/test-suite/modules/pliczek.v +++ b/test-suite/modules/pliczek.v @@ -1,3 +1,3 @@ Require Export plik. -Definition tutu (X : Set) := toto X.
\ No newline at end of file +Definition tutu (X : Set) := toto X. diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v index 50bfd96046..c2f0fe3cee 100644 --- a/test-suite/modules/plik.v +++ b/test-suite/modules/plik.v @@ -1,3 +1,3 @@ Definition toto (x : Set) := x. -(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file +(* <Warning> : Grammar is replaced by Notation *) diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v index 9e46d17ed9..6bf067fd18 100644 --- a/test-suite/modules/pseudo_circular_with.v +++ b/test-suite/modules/pseudo_circular_with.v @@ -3,4 +3,4 @@ Module Type T. Declare Module M:S. End T. Module N:S. End N. Module NN:T. Module M:=N. End NN. -Module Type U := T with Module M:=NN.
\ No newline at end of file +Module Type U := T with Module M:=NN. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index da5d25fa2e..fc936a515a 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -26,4 +26,4 @@ Module Type SIG. Parameter x : T. End SIG. -Module J : SIG := M.N.
\ No newline at end of file +Module J : SIG := M.N. diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v index 07588d34f9..c409c0ee46 100644 --- a/test-suite/output/CompactContexts.v +++ b/test-suite/output/CompactContexts.v @@ -2,4 +2,4 @@ Set Printing Compact Contexts. Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False. Show. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 9d106d2dac..7bcd7b041c 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with | 1 => 1 end = p : forall x : nat, x = x -> Prop +bar 0 + : nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b9985a594f..fe6c05c39e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e5dbfcb4be..65efe228af 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -122,3 +122,5 @@ return (1, 2, 3, 4) : nat * nat * nat * nat {{ 1 | 1 // 1 }} : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b1015137d6..ea372ad1a3 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4). Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. + +(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) +Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). +Check !!! (x y:nat), True. diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v index bde195a511..de9f48873a 100644 --- a/test-suite/output/SearchPattern.v +++ b/test-suite/output/SearchPattern.v @@ -33,4 +33,4 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False. Search (P _) -"h'". (* search hypothesis also for patterns *) Search (P _) -not. (* search hypothesis also for patterns *) -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v index 8ecd97aa56..91331a1de5 100644 --- a/test-suite/output/ltac_missing_args.v +++ b/test-suite/output/ltac_missing_args.v @@ -16,4 +16,4 @@ Goal True. Fail (fun _ => idtac). Fail rec True. Fail let rec tac x := tac in tac True. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 837f2efd06..4d04f2cf9b 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing). Reserved Notation "x === y" (at level 50). Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x where "x === y" := (EQ x y). + +(* Check that strictly ident or _ are coerced to a name *) + +Fail Check {x@{u},y|x=x}. +Fail Check {?[n],y|0=0}. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 681c4716b6..85d7a770fc 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -102,4 +102,4 @@ Qed. Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) {measure (p - n) p} : nat := - _.
\ No newline at end of file + _. diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v index 6aeb05f54e..c98689c234 100644 --- a/test-suite/success/cbn.v +++ b/test-suite/success/cbn.v @@ -15,4 +15,4 @@ Goal forall n, foo (S n) = g n. match goal with |- g _ = g _ => reflexivity end. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index e25510cf09..03034cf130 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -30,4 +30,4 @@ Section Foo. assert(b:=Build_A). solve [ typeclasses eauto ]. Qed. -End Foo.
\ No newline at end of file +End Foo. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index b538d2ed27..9b11bc011c 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -130,4 +130,4 @@ Local Coercion l2v2 : list >-> vect. of coercions *) Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). -Section what_we_could_do.
\ No newline at end of file +Section what_we_could_do. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v index f5c25540ef..2bc3f9d22a 100644 --- a/test-suite/success/hintdb_in_ltac_bis.v +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -12,4 +12,4 @@ Goal Foo. progress foo mybase. Undo. progress bar mybase. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v index 91b6dee2ec..a962c29f44 100644 --- a/test-suite/success/indelim.v +++ b/test-suite/success/indelim.v @@ -58,4 +58,4 @@ Inductive color := Red | Black. Inductive option (A : Type) : Type := | None : option A -| Some : A -> option A.
\ No newline at end of file +| Some : A -> option A. diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index b88c142be1..5638a7d3eb 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -59,4 +59,4 @@ Qed. Lemma test b : b && true = b. Fail rewrite andb_true_l. Admitted. -
\ No newline at end of file + diff --git a/test-suite/success/ltac_match_pattern_names.v b/test-suite/success/ltac_match_pattern_names.v index 7363294960..790cd1b3a7 100644 --- a/test-suite/success/ltac_match_pattern_names.v +++ b/test-suite/success/ltac_match_pattern_names.v @@ -25,4 +25,4 @@ Ltac multiple_branches := let P := fresh P in let Q := fresh Q in idtac - end.
\ No newline at end of file + end. diff --git a/test-suite/success/ltac_plus.v b/test-suite/success/ltac_plus.v index 8a08d64650..01d477bdf9 100644 --- a/test-suite/success/ltac_plus.v +++ b/test-suite/success/ltac_plus.v @@ -9,4 +9,4 @@ Proof. Fail ((apply h0+apply h2) || apply h1); apply h3. (* interaction with || *) ((apply h0+apply h1) || apply h2); apply h3. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v index 414c572f81..05f4a71856 100644 --- a/test-suite/success/programequality.v +++ b/test-suite/success/programequality.v @@ -10,4 +10,4 @@ Proof. pi_eq_proofs. clear e. destruct e'. simpl. change (P a eq_refl). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v index d0aafd3833..d73864e4e0 100644 --- a/test-suite/success/rewrite_dep.v +++ b/test-suite/success/rewrite_dep.v @@ -31,4 +31,4 @@ Proof. intros. rewrite H0. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v index 04c675563e..a6e59fdda0 100644 --- a/test-suite/success/rewrite_strat.v +++ b/test-suite/success/rewrite_strat.v @@ -50,4 +50,4 @@ Proof. Time Qed. (* 0.06 s *) Set Printing All. -Set Printing Depth 100000.
\ No newline at end of file +Set Printing Depth 100000. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 269359ae62..fc74225d76 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -76,4 +76,4 @@ End Ind. Module Rec. Record box_in : myType := BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. -End Rec.
\ No newline at end of file +End Rec. diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v index 439782c9e5..1394477027 100644 --- a/test-suite/typeclasses/deftwice.v +++ b/test-suite/typeclasses/deftwice.v @@ -6,4 +6,4 @@ Instance inhab_C : C Type := Inhab. Variable full : forall A (X : C A), forall x : A, c x. -Definition truc {A : Type} : Inhab A := (full _ _ _).
\ No newline at end of file +Definition truc {A : Type} : Inhab A := (full _ _ _). diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v index 663a837f36..518912433d 100644 --- a/test-suite/typeclasses/unification_delta.v +++ b/test-suite/typeclasses/unification_delta.v @@ -43,4 +43,4 @@ Proof. (* Breaks if too much delta in unification *) rewrite H. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 88cda79d82..247ea20a88 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -57,4 +57,4 @@ now rewrite H. Qed. (** For compatibility *) -Require Import Le Lt.
\ No newline at end of file +Require Import Le Lt. diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index 572f286545..e03fb2236a 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -20,4 +20,4 @@ Require Export FSetEqProperties. Require Export FSetWeakList. Require Export FSetList. Require Export FSetPositive. -Require Export FSetAVL.
\ No newline at end of file +Require Export FSetAVL. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index f7b53f1dc2..a5ae07b64c 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -97,12 +97,12 @@ Proof proof_irrelevance_cci classic. (* classical_left transforms |- A \/ B into ~B |- A *) (* classical_right transforms |- A \/ B into ~A |- B *) -Ltac classical_right := match goal with - | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +Ltac classical_right := match goal with +|- ?X \/ _ => (elim (classic X);intro;[left;trivial|right]) end. Ltac classical_left := match goal with -| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +|- _ \/ ?X => (elim (classic X);intro;[right;trivial|left]) end. Require Export EqdepFacts. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 036ff1aa4b..9fb8e499ba 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -1144,4 +1144,4 @@ Proof. apply mindepth_cardinal. Qed. -End Props.
\ No newline at end of file +End Props. diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v index f179bcd1d7..1ee485cc13 100644 --- a/theories/MSets/MSets.v +++ b/theories/MSets/MSets.v @@ -18,4 +18,4 @@ Require Export MSetEqProperties. Require Export MSetWeakList. Require Export MSetList. Require Export MSetPositive. -Require Export MSetAVL.
\ No newline at end of file +Require Export MSetAVL. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index ba923d0624..6771e57add 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -378,4 +378,4 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A := | pos p => Pos.iter f x p end. -End N.
\ No newline at end of file +End N. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index de3bbbca76..626d59d73e 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -260,4 +260,4 @@ Proof. intros. apply odd_add_mul_even. apply even_spec, even_2. Qed. -End NZParityProp.
\ No newline at end of file +End NZParityProp. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 9aca56f479..b06562fc4f 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -328,4 +328,4 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; tr Obligation Tactic := program_simpl. -Definition obligation (A : Type) {a : A} := a.
\ No newline at end of file +Definition obligation (A : Type) {a : A} := a. diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v index 1883c77be5..09908665e1 100644 --- a/theories/QArith/Qcabs.v +++ b/theories/QArith/Qcabs.v @@ -126,4 +126,4 @@ Proof. destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B]. + rewrite H; apply Qcle_refl. + apply Qcle_antisym; auto. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 66e37e867e..9b0357f033 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -26,4 +26,4 @@ Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. -Require Export Ranalysis_reg.
\ No newline at end of file +Require Export Ranalysis_reg. diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v index 672858fa51..19d749fc85 100644 --- a/theories/Vectors/Vector.v +++ b/theories/Vectors/Vector.v @@ -21,4 +21,4 @@ Require VectorSpec. Require VectorEq. Include VectorDef. Include VectorSpec. -Include VectorEq.
\ No newline at end of file +Include VectorEq. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 7686fbae87..443667f48b 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -616,4 +616,4 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -End Z.
\ No newline at end of file +End Z. diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index fb7f71b4b5..cccd970dad 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -229,4 +229,4 @@ Proof. symmetry. apply Z.sqrt_unique; trivial. now apply Zsqrt_interval. now destruct n. -Qed.
\ No newline at end of file +Qed. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f4d1118d0f..56e12a1e06 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -207,8 +207,8 @@ else TIMING_ARG= endif -# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) -ifneq "$(DSTROOT)" "" +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT DESTDIR := $(DSTROOT) endif diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 2be10a0397..e15911dd65 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i = pr_inductive (Global.env()) (fst i) ++ str "." let error_not_allowed_dependent_analysis isrec i = - str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str "." diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6ea8bc7f2c..facebd096a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -30,7 +30,6 @@ open Globnames open Goptions open Nameops open Termops -open Pretyping open Nametab open Smartlocate open Vernacexpr @@ -345,24 +344,23 @@ requested let names inds recs isdep y z = let ind = smart_global_inductive y in let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in - let z' = interp_elimination_sort z in let suffix = ( match sort_of_ind with | InProp -> - if isdep then (match z' with + if isdep then (match z with | InProp -> inds ^ "_dep" | InSet -> recs ^ "_dep" | InType -> recs ^ "t_dep") - else ( match z' with + else ( match z with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) | _ -> - if isdep then (match z' with + if isdep then (match z with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) - else (match z' with + else (match z with | InProp -> inds ^ "_nodep" | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") @@ -392,7 +390,7 @@ let do_mutual_induction_scheme lnamedepindsort = evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst in - (evd, (indu,dep,interp_elimination_sort sort) :: l, inst)) + (evd, (indu,dep,sort) :: l, inst)) lnamedepindsort (Evd.from_env env0,[],None) in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 076e4938fd..91c4c58255 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -11,7 +11,6 @@ open Names open Term open Environ open Vernacexpr -open Misctypes (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) @@ -32,7 +31,7 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (Id.t located * bool * inductive * glob_sort) list -> unit + (Id.t located * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8b042a3ca3..c424b1d501 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -98,8 +98,7 @@ let pr_grammar = function quote (except a single quote alone) must be quoted) *) let parse_format ((loc, str) : lstring) = - let str = " "^str in - let l = String.length str in + let len = String.length str in let push_token a = function | cur::l -> (a::cur)::l | [] -> [[a]] in @@ -109,16 +108,16 @@ let parse_format ((loc, str) : lstring) = | a::(_::_ as l) -> push_token (UnpBox (b,a)) l | _ -> user_err Pp.(str "Non terminated box in format.") in let close_quotation i = - if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') + if i < len && str.[i] == '\'' && (Int.equal (i+1) len || str.[i+1] == ' ') then i+1 else user_err Pp.(str "Incorrectly terminated quoted expression.") in let rec spaces n i = - if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) + if i < len && str.[i] == ' ' then spaces (n+1) (i+1) else n in let rec nonspaces quoted n i = - if i < String.length str && str.[i] != ' ' then + if i < len && str.[i] != ' ' then if str.[i] == '\'' && quoted && - (i+1 >= String.length str || str.[i+1] == ' ') + (i+1 >= len || str.[i+1] == ' ') then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else @@ -126,26 +125,26 @@ let parse_format ((loc, str) : lstring) = else n in let rec parse_non_format i = let n = nonspaces false 0 i in - push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n)) + push_token (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) and parse_quoted n i = - if i < String.length str then match str.[i] with + if i < len then match str.[i] with (* Parse " // " *) - | '/' when i <= String.length str && str.[i+1] == '/' -> + | '/' when i <= len && str.[i+1] == '/' -> (* We forget the useless n spaces... *) push_token (UnpCut PpFnl) - (parse_token (close_quotation (i+2))) + (parse_token 1 (close_quotation (i+2))) (* Parse " .. / .. " *) - | '/' when i <= String.length str -> + | '/' when i <= len -> let p = spaces 0 (i+1) in push_token (UnpCut (PpBrk (n,p))) - (parse_token (close_quotation (i+p+1))) + (parse_token 1 (close_quotation (i+p+1))) | c -> (* The spaces are real spaces *) push_white n (match c with | '[' -> - if i <= String.length str then match str.[i+1] with + if i <= len then match str.[i+1] with (* Parse " [h .. ", *) - | 'h' when i+1 <= String.length str && str.[i+2] == 'v' -> + | 'h' when i+1 <= len && str.[i+2] == 'v' -> (parse_box (fun n -> PpHVB n) (i+3)) (* Parse " [v .. ", *) | 'v' -> @@ -157,39 +156,39 @@ let parse_format ((loc, str) : lstring) = else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> - ([] :: parse_token (close_quotation (i+1))) + ([] :: parse_token 1 (close_quotation (i+1))) (* Parse a non formatting token *) | c -> let n = nonspaces true 0 i in push_token (UnpTerminal (String.sub str (i-1) (n+2))) - (parse_token (close_quotation (i+n)))) + (parse_token 1 (close_quotation (i+n)))) else if Int.equal n 0 then [] else user_err Pp.(str "Ending spaces non part of a format annotation.") and parse_box box i = let n = spaces 0 i in - close_box i (box n) (parse_token (close_quotation (i+n))) - and parse_token i = + close_box i (box n) (parse_token 1 (close_quotation (i+n))) + and parse_token k i = let n = spaces 0 i in let i = i+n in - if i < l then match str.[i] with + if i < len then match str.[i] with (* Parse a ' *) - | '\'' when i+1 >= String.length str || str.[i+1] == ' ' -> - push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1))) + | '\'' when i+1 >= len || str.[i+1] == ' ' -> + push_white (n-k) (push_token (UnpTerminal "'") (parse_token 1 (i+1))) (* Parse the beginning of a quoted expression *) | '\'' -> - parse_quoted (n-1) (i+1) + parse_quoted (n-k) (i+1) (* Otherwise *) | _ -> - push_white (n-1) (parse_non_format i) + push_white (n-k) (parse_non_format i) else push_white n [[]] in try - if not (String.is_empty str) then match parse_token 0 with + if not (String.is_empty str) then match parse_token 0 0 with | [l] -> l | _ -> user_err Pp.(str "Box closed without being opened in format.") else - user_err Pp.(str "Empty format.") + [] with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in |