aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/cStack.ml44
-rw-r--r--clib/cStack.mli58
-rw-r--r--clib/clib.mllib2
-rw-r--r--lib/util.ml4
-rw-r--r--lib/util.mli4
-rw-r--r--plugins/cc/ccalgo.mli97
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--test-suite/bugs/closed/bug_11730.v6
-rw-r--r--test-suite/bugs/closed/bug_9512.v7
-rw-r--r--test-suite/bugs/closed/bug_9930.v14
-rw-r--r--vernac/metasyntax.ml2
11 files changed, 31 insertions, 217 deletions
diff --git a/clib/cStack.ml b/clib/cStack.ml
deleted file mode 100644
index 0432e29fad..0000000000
--- a/clib/cStack.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-exception Empty = Stack.Empty
-
-type 'a t = {
- mutable stack : 'a list;
-}
-
-let create () = { stack = [] }
-
-let push x s = s.stack <- x :: s.stack
-
-let pop = function
- | { stack = [] } -> raise Stack.Empty
- | { stack = x::xs } as s -> s.stack <- xs; x
-
-let top = function
- | { stack = [] } -> raise Stack.Empty
- | { stack = x::_ } -> x
-
-let to_list { stack = s } = s
-
-let find f s = List.find f (to_list s)
-
-let find_map f s = CList.find_map f s.stack
-
-let fold_until f accu s = CList.fold_left_until f accu s.stack
-
-let is_empty { stack = s } = s = []
-
-let iter f { stack = s } = List.iter f s
-
-let clear s = s.stack <- []
-
-let length { stack = s } = List.length s
-
diff --git a/clib/cStack.mli b/clib/cStack.mli
deleted file mode 100644
index de802160e7..0000000000
--- a/clib/cStack.mli
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Extended interface for OCaml stacks. *)
-
-type 'a t
-
-exception Empty
-(** Alias for Stack.Empty. *)
-
-val create : unit -> 'a t
-(** Create an empty stack. *)
-
-val push : 'a -> 'a t -> unit
-(** Add an element to a stack. *)
-
-val find : ('a -> bool) -> 'a t -> 'a
-(** Find the first element satisfying the predicate.
- @raise Not_found it there is none. *)
-
-val is_empty : 'a t -> bool
-(** Whether a stack is empty. *)
-
-val iter : ('a -> unit) -> 'a t -> unit
-(** Iterate a function over elements, from the last added one. *)
-
-val clear : 'a t -> unit
-(** Empty a stack. *)
-
-val length : 'a t -> int
-(** Length of a stack. *)
-
-val pop : 'a t -> 'a
-(** Remove and returns the first element of the stack.
- @raise Empty if empty. *)
-
-val top : 'a t -> 'a
-(** Remove the first element of the stack without modifying it.
- @raise Empty if empty. *)
-
-val to_list : 'a t -> 'a list
-(** Convert to a list. *)
-
-val find_map : ('a -> 'b option) -> 'a t -> 'b
-(** Find the first element that returns [Some _].
- @raise Not_found it there is none. *)
-
-val fold_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a t -> 'c
-(** Like CList.fold_left_until.
- The stack is traversed from the top and is not altered. *)
-
diff --git a/clib/clib.mllib b/clib/clib.mllib
index 5a2c9a9ce9..be3b5971be 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -9,7 +9,6 @@ CSet
CMap
CList
CString
-CStack
Int
Range
@@ -33,7 +32,6 @@ Unionfind
Dyn
Store
Exninfo
-Backtrace
IStream
Terminal
Monad
diff --git a/lib/util.ml b/lib/util.ml
index e2447b005e..ae8119ced0 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -82,10 +82,6 @@ module Set = CSet
module Map = CMap
-(* Stacks *)
-
-module Stack = CStack
-
(* Matrices *)
let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index 1417d6dfcb..be0cc11763 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -76,10 +76,6 @@ module Set : module type of CSet
module Map : module type of CMap
-(** {6 Stacks.} *)
-
-module Stack : module type of CStack
-
(** {6 Streams. } *)
val stream_nth : int -> 'a Stream.t -> 'a
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3dc934b426..b0b74f4558 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Constr
open Names
@@ -156,102 +155,6 @@ val subterms : forest -> int -> int * int
val join_path : forest -> int -> int ->
((int * int) * equality) list * ((int * int) * equality) list
-val make_fun_table : state -> Int.Set.t PafMap.t
-
-val do_match : state ->
- (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
-
-val init_pb_stack : state -> matching_problem Stack.t
-
-val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun
-
-val find_instances : state -> (quant_eq * int array) list
-
val execute : bool -> state -> explanation option
val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
-
-val empty_forest: unit -> forest
-
-
-
-
-
-
-
-
-
-
-(*type pa_constructor
-
-
-module PacMap:CSig.MapS with type key=pa_constructor
-
-type term =
- Symb of Term.constr
- | Eps
- | Appli of term * term
- | Constructor of Names.constructor*int*int
-
-type rule =
- Congruence
- | Axiom of Names.Id.t
- | Injection of int*int*int*int
-
-type equality =
- {lhs : int;
- rhs : int;
- rule : rule}
-
-module ST :
-sig
- type t
- val empty : unit -> t
- val enter : int -> int * int -> t -> unit
- val query : int * int -> t -> int
- val delete : int -> t -> unit
- val delete_list : int list -> t -> unit
-end
-
-module UF :
-sig
- type t
- exception Discriminable of int * int * int * int * t
- val empty : unit -> t
- val find : t -> int -> int
- val size : t -> int -> int
- val get_constructor : t -> int -> Names.constructor
- val pac_arity : t -> int -> int * int -> int
- val mem_node_pac : t -> int -> int * int -> int
- val add_pacs : t -> int -> pa_constructor PacMap.t ->
- int list * equality list
- val term : t -> int -> term
- val subterms : t -> int -> int * int
- val add : t -> term -> int
- val union : t -> int -> int -> equality -> int list * equality list
- val join_path : t -> int -> int ->
- ((int*int)*equality) list*
- ((int*int)*equality) list
-end
-
-
-val combine_rec : UF.t -> int list -> equality list
-val process_rec : UF.t -> equality list -> int list
-
-val cc : UF.t -> unit
-
-val make_uf :
- (Names.Id.t * (term * term)) list -> UF.t
-
-val add_one_diseq : UF.t -> (term * term) -> int * int
-
-val add_disaxioms :
- UF.t -> (Names.Id.t * (term * term)) list ->
- (Names.Id.t * (int * int)) list
-
-val check_equal : UF.t -> int * int -> bool
-
-val find_contradiction : UF.t ->
- (Names.Id.t * (int * int)) list ->
- (Names.Id.t * (int * int))
-*)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4afed07eda..fdf0db9909 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1009,11 +1009,11 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in
let app' = f acc app in
let a' = f acc a in
- (match EConstr.kind sigma app' with
- | App (hdf', al') when hdf' == hdf ->
- (* Still the same projection, we ignore the change in parameters *)
- mkProj (p, a')
- | _ -> mkApp (app', [| a' |]))
+ let hdf', _ = decompose_app_vect sigma app' in
+ if hdf' == hdf then
+ (* Still the same projection, we ignore the change in parameters *)
+ mkProj (p, a')
+ else mkApp (app', [| a' |])
| _ -> map_constr_with_binders_left_to_right sigma g f acc c
let e_contextually byhead (occs,c) f = begin fun env sigma t ->
diff --git a/test-suite/bugs/closed/bug_11730.v b/test-suite/bugs/closed/bug_11730.v
new file mode 100644
index 0000000000..f788636f9c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11730.v
@@ -0,0 +1,6 @@
+Set Mangle Names.
+
+Infix "&&&" := andb (at level 40, left associativity).
+(* Error: Variable _0 occurs more than once. *)
+
+Check (_ &&& _).
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index 25285622a9..bad9d64f65 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -4,9 +4,10 @@ Set Primitive Projections.
Record params := { width : Z }.
Definition p : params := Build_params 64.
+Definition width' := width.
Set Printing All.
-Goal width p = 0%Z -> width p = 0%Z.
+Lemma foo : width p = 0%Z -> width p = 0%Z.
intros.
assert_succeeds (enough True; [omega|]).
@@ -16,7 +17,9 @@ Goal width p = 0%Z -> width p = 0%Z.
(* ============================ *)
(* @eq Z (width p) Z0 *)
- change tt with tt in H.
+ change (width' p = 0%Z) in H;cbv [width'] in H.
+ (* check that we correctly got the compat constant in H *)
+ Fail match goal with H : ?l = _ |- ?l' = _ => constr_eq l l' end.
(* H : @eq Z (width p) Z0 *)
(* ============================ *)
diff --git a/test-suite/bugs/closed/bug_9930.v b/test-suite/bugs/closed/bug_9930.v
new file mode 100644
index 0000000000..042cd69fbe
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9930.v
@@ -0,0 +1,14 @@
+Set Primitive Projections.
+Record params := { width : nat }.
+Definition p : params := Build_params 64.
+
+Lemma foo : width p = 0 -> width p = 0.
+ intros.
+ let e := lazymatch type of H with ?e = 0 => e end in
+ change tt with tt in H;
+ let E := lazymatch type of H with ?E = 0 => E end in
+ idtac "before:" e; idtac "after :" E;
+ (* before: (width p) *)
+ (* after : (width p) *)
+ tryif constr_eq e E then exact H else idtac.
+Qed.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 33fd14a731..10946d78f0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1708,7 +1708,7 @@ let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
(* check the precedence *)
let vars = names_of_constr_expr pr in
let x = Namegen.next_ident_away (Id.of_string "x") vars in
- let y = Namegen.next_ident_away (Id.of_string "y") vars in
+ let y = Namegen.next_ident_away (Id.of_string "y") (Id.Set.add x vars) in
let metas = [inject_var x; inject_var y] in
let c = mkAppC (pr,metas) in
let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 19:22:50 +0000