aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/loadpath.ml3
-rw-r--r--ltac/g_class.ml414
-rw-r--r--ltac/profile_ltac.ml17
-rw-r--r--ltac/profile_ltac.mli3
-rw-r--r--ltac/profile_ltac_tactics.ml43
-rw-r--r--plugins/nsatz/ideal.ml74
-rw-r--r--pretyping/cases.ml100
-rw-r--r--pretyping/vnorm.ml6
-rw-r--r--printing/printer.ml3
-rw-r--r--proofs/logic.ml14
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli1
-rw-r--r--tactics/tactics.ml15
-rw-r--r--test-suite/bugs/closed/4785.v45
-rw-r--r--test-suite/bugs/closed/5093.v11
-rw-r--r--test-suite/bugs/closed/5096.v219
-rw-r--r--test-suite/success/Case13.v38
-rw-r--r--theories/Compat/Coq84.v4
-rw-r--r--theories/Compat/Coq85.v20
-rw-r--r--theories/Lists/List.v10
-rw-r--r--theories/Vectors/VectorDef.v11
-rw-r--r--toplevel/coqinit.ml2
24 files changed, 482 insertions, 139 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml
index e6f6716c3..d03c6c555 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit =
let replace =
if DirPath.equal coq_path old_path then
implicit <> old_implicit
- else if DirPath.equal coq_path (Nameops.default_root_prefix)
- && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
- false (* This is the default "-I ." path, don't override the old path *)
else
let () =
(* Do not warn when overriding the default "-I ." path *)
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index d551b7315..f8654d390 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
| [ ] -> [ false ]
END
-let pr_depth _prc _prlc _prt = function
- Some i -> Pp.int i
- | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
- | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
set_typeclasses_debug d;
set_typeclasses_depth depth
]
@@ -63,9 +55,9 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
[ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
END
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index fe591c775..102918e5e 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -166,7 +166,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
and print_table ~filter all_total indent first_level table =
let fold _ n l =
let s, total = n.name, n.total in
- if filter s then (s, n) :: l else l in
+ if filter s total then (s, n) :: l else l in
let ls = M.fold fold table [] in
match ls with
| [s, n] when not first_level ->
@@ -182,7 +182,7 @@ and print_table ~filter all_total indent first_level table =
in
prlist (fun pr -> pr) (list_iter_is_last iter ls)
-let to_string ~filter node =
+let to_string ~filter ?(cutoff=0.0) node =
let tree = node.children in
let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
let flat_tree =
@@ -218,6 +218,7 @@ let to_string ~filter node =
!global
in
warn_encountered_multi_success_backtracking ();
+ let filter s n = filter s && n >= cutoff in
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
@@ -387,22 +388,24 @@ let reset_profile () =
(* ******************** *)
-let print_results_filter ~filter =
+let print_results_filter ~cutoff ~filter =
let valid id _ = Stm.state_of_id id <> `Expired in
data := SM.filter valid !data;
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results Local.(CList.last !stack) in
- Feedback.msg_notice (to_string ~filter results)
+ Feedback.msg_notice (to_string ~cutoff ~filter results)
;;
-let print_results () = print_results_filter ~filter:(fun _ -> true)
+let print_results ~cutoff =
+ print_results_filter ~cutoff ~filter:(fun _ -> true)
let print_results_tactic tactic =
- print_results_filter ~filter:(fun s ->
+ print_results_filter ~cutoff:0.0 ~filter:(fun s ->
String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
-let do_print_results_at_close () = if get_profiling () then print_results ()
+let do_print_results_at_close () =
+ if get_profiling () then print_results ~cutoff:0.0
let _ = Declaremods.append_end_library_hook do_print_results_at_close
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8c4b47b8e..e5e2e4197 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -14,7 +14,8 @@ val do_profile :
val set_profiling : bool -> unit
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
val print_results_tactic : string -> unit
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb6..9083bda60 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
- [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
END
VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 482ce5053..7c2178222 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -127,11 +127,11 @@ type polynom =
num : int;
sugar : int}
-let nvar m = Array.length m - 1
+let nvar (m : mon) = Array.length m - 1
-let deg m = m.(0)
+let deg (m : mon) = m.(0)
-let mult_mon m m' =
+let mult_mon (m : mon) (m' : mon) =
let d = nvar m in
let m'' = Array.make (d+1) 0 in
for i=0 to d do
@@ -140,7 +140,7 @@ let mult_mon m m' =
m''
-let compare_mon m m' =
+let compare_mon (m : mon) (m' : mon) =
let d = nvar m in
if !lexico
then (
@@ -148,18 +148,18 @@ let compare_mon m m' =
let res=ref 0 in
let i=ref 1 in (* 1 si lexico pur 0 si degre*)
while (!res=0) && (!i<=d) do
- res:= (compare m.(!i) m'.(!i));
+ res:= (Int.compare m.(!i) m'.(!i));
i:=!i+1;
done;
!res)
else (
(* degre lexicographique inverse *)
- match compare m.(0) m'.(0) with
+ match Int.compare m.(0) m'.(0) with
| 0 -> (* meme degre total *)
let res=ref 0 in
let i=ref d in
while (!res=0) && (!i>=1) do
- res:= - (compare m.(!i) m'.(!i));
+ res:= - (Int.compare m.(!i) m'.(!i));
i:=!i-1;
done;
!res
@@ -402,29 +402,25 @@ let polconst d c =
[(c,m)]
let plusP p q =
- let rec plusP p q =
- match p with
- [] -> q
- |t::p' ->
- match q with
- [] -> p
- |t'::q' ->
- match compare_mon (snd t) (snd t') with
- 1 -> t::(plusP p' q)
- |(-1) -> t'::(plusP p q')
- |_ -> let c=P.plusP (fst t) (fst t') in
- match P.equal c coef0 with
- true -> (plusP p' q')
- |false -> (c,(snd t))::(plusP p' q')
- in plusP p q
+ let rec plusP p q accu = match p, q with
+ | [], [] -> List.rev accu
+ | [], _ -> List.rev_append accu q
+ | _, [] -> List.rev_append accu p
+ | t :: p', t' :: q' ->
+ let c = compare_mon (snd t) (snd t') in
+ if c > 0 then plusP p' q (t :: accu)
+ else if c < 0 then plusP p q' (t' :: accu)
+ else
+ let c = P.plusP (fst t) (fst t') in
+ if P.equal c coef0 then plusP p' q' accu
+ else plusP p' q' ((c, (snd t)) :: accu)
+ in
+ plusP p q []
(* multiplication by (a,monomial) *)
let mult_t_pol a m p =
- let rec mult_t_pol p =
- match p with
- [] -> []
- |(b,m')::p -> ((P.multP a b),(mult_mon m m'))::(mult_t_pol p)
- in mult_t_pol p
+ let map (b, m') = (P.multP a b, mult_mon m m') in
+ CList.map map p
let coef_of_int x = P.of_num (Num.Int x)
@@ -451,23 +447,27 @@ let emultP a p =
in emultP p
let multP p q =
- let rec aux p =
+ let rec aux p accu =
match p with
- [] -> []
- |(a,m)::p' -> plusP (mult_t_pol a m q) (aux p')
- in aux p
+ [] -> accu
+ |(a,m)::p' -> aux p' (plusP (mult_t_pol a m q) accu)
+ in aux p []
let puisP p n=
match p with
[] -> []
|_ ->
+ if n = 0 then
let d = nvar (snd (List.hd p)) in
- let rec puisP n =
- match n with
- 0 -> [coef1, Array.make (d+1) 0]
- | 1 -> p
- |_ -> multP p (puisP (n-1))
- in puisP n
+ [coef1, Array.make (d+1) 0]
+ else
+ let rec puisP p n =
+ if n = 1 then p
+ else
+ let q = puisP p (n / 2) in
+ let q = multP q q in
+ if n mod 2 = 0 then q else multP p q
+ in puisP p n
let rec contentP p =
match p with
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad57c1643..72baa3493 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,16 +1870,22 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
+let add_subst c len (rel_subst,var_subst) =
+ match kind_of_term c with
+ | Rel n -> (n,len) :: rel_subst, var_subst
+ | Var id -> rel_subst, (id,len) :: var_subst
+ | _ -> assert false
+
let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
- let subst, len =
+ let (rel_subst,var_subst), len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match kind_of_term tm with
- | Rel n when dependent tm c
+ | Rel _ | Var _ when dependent tm c
&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
- ((n, len) :: subst, len - signlen)
- | Rel n when signlen > 1 (* The term is of a dependent type,
+ (add_subst tm len subst, len - signlen)
+ | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
maybe some variable in its type appears in the tycon. *) ->
(match tmtype with
NotInd _ -> (subst, len - signlen)
@@ -1888,28 +1894,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_left
(fun (subst, len) arg ->
match kind_of_term arg with
- | Rel n when dependent arg c ->
- ((n, len) :: subst, pred len)
+ | Rel _ | Var _ when dependent arg c ->
+ (add_subst arg len subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent tm c && List.for_all isRel realargs
- then (n, len) :: subst else subst
+ if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
+ then add_subst tm len subst else subst
in (subst, pred len))
| _ -> (subst, len - signlen))
- (List.rev tomatchs) arsign ([], nar)
+ (List.rev tomatchs) arsign (([],[]), nar)
in
let rec predicate lift c =
match kind_of_term c with
| Rel n when n > lift ->
(try
(* Make the predicate dependent on the matched variable *)
- let idx = Int.List.assoc (n - lift) subst in
+ let idx = Int.List.assoc (n - lift) rel_subst in
mkRel (idx + lift)
with Not_found ->
- (* A variable that is not matched, lift over the arsign. *)
+ (* A variable that is not matched, lift over the arsign *)
mkRel (n + nar))
+ | Var id ->
+ (try
+ (* Make the predicate dependent on the matched variable *)
+ let idx = Id.List.assoc id var_subst in
+ mkRel (idx + lift)
+ with Not_found ->
+ (* A variable that is not matched *)
+ c)
| _ ->
map_constr_with_binders succ predicate lift c
in
@@ -1925,46 +1939,44 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
* type and 1 assumption for each term not _syntactically_ in an
* inductive type.
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: we try to specialize the
- * tycon to make the predicate if it is not closed.
+ * Each matched term is independently considered dependent or not.
*)
let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let preds =
- match pred, tycon with
+ match pred with
(* No return clause *)
- | None, Some t when not (noccur_with_meta 0 max_int t) ->
- (* If the tycon is not closed w.r.t real variables, we try *)
- (* two different strategies *)
- (* First strategy: we abstract the tycon wrt to the dependencies *)
- let p1 =
- prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
- (* Second strategy: we build an "inversion" predicate *)
- let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
- (match p1 with
- | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
- | None -> [sigma2, pred2])
- | None, _ ->
- (* No dependent type constraint, or no constraints at all: *)
- (* we use two strategies *)
- let sigma,t = match tycon with
- | Some t -> sigma,t
- | None ->
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma ((t, _), sigma, _) =
- new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
- let sigma = Sigma.to_evar_map sigma in
- sigma, t
- in
- (* First strategy: we build an "inversion" predicate *)
+ | None ->
+ let sigma,t =
+ match tycon with
+ | Some t -> sigma, t
+ | None ->
+ (* No type constraint: we first create a generic evar type constraint *)
+ let src = (loc, Evar_kinds.CasesType false) in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
+ let sigma = Sigma.to_evar_map sigma in
+ sigma, t in
+ (* First strategy: we build an "inversion" predicate, also replacing the *)
+ (* dependencies with existential variables *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
- (* Second strategy: we directly use the evar as a non dependent pred *)
- let pred2 = lift (List.length (List.flatten arsign)) t in
- [sigma1, pred1; sigma, pred2]
+ (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
+ let p2 =
+ prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+ (* Third strategy: we take the type constraint as it is; of course we could *)
+ (* need something inbetween, abstracting some but not all of the dependencies *)
+ (* the "inversion" strategy deals with that but unification may not be *)
+ (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
+ (* work (yet) when a constructor has a type not precise enough for the inversion *)
+ (* see log message for details *)
+ let pred3 = lift (List.length (List.flatten arsign)) t in
+ (match p2 with
+ | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
+ [sigma1, pred1; sigma2, pred2; sigma, pred3]
+ | _ ->
+ [sigma1, pred1; sigma, pred3])
(* Some type annotation *)
- | Some rtntyp, _ ->
+ | Some rtntyp ->
(* We extract the signature of the arity *)
let envar = List.fold_right push_rel_context arsign env in
let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 331ad0912..75159bf8b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -49,7 +49,11 @@ let invert_tag cst tag reloc_tbl =
with Find_at j -> (j+1)
(* Argggg, ces constructeurs de ... qui commencent a 1*)
-let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c
+let find_rectype_a env c =
+ let (t, l) = decompose_appvect (whd_all env c) in
+ match kind_of_term t with
+ | Ind ind -> (ind, l)
+ | _ -> assert false
(* Instantiate inductives and parameters in constructor type *)
diff --git a/printing/printer.ml b/printing/printer.ml
index a6c7c5ca1..52cb07b8f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -735,9 +735,6 @@ let pr_prim_rule = function
str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
- | Move (id1,id2) ->
- (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
-
(* Backwards compatibility *)
let prterm = pr_lconstr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5aba6b614..d23a4ad61 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -278,6 +278,11 @@ let move_hyp toleft (left,declfrom,right) hto =
List.fold_left (fun sign d -> push_named_context_val d sign)
right left
+let move_hyp_in_named_context hfrom hto sign =
+ let (left,right,declfrom,toleft) =
+ split_sign hfrom hto (named_context_of_val sign) in
+ move_hyp toleft (left,declfrom,right) hto
+
(**********************************************************************)
@@ -552,12 +557,3 @@ let prim_refiner r sigma goal =
let sgl = List.rev sgl in
let sigma = Goal.V82.partial_solution sigma goal oterm in
(sgl, sigma)
-
- | Move (hfrom, hto) ->
- let (left,right,declfrom,toleft) =
- split_sign hfrom hto (named_context_of_val sign) in
- let hyps' =
- move_hyp toleft (left,declfrom,right) hto in
- let (gl,ev,sigma) = mk_goal hyps' cl in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
- ([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2764d28c0..0dba9ef1e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -56,3 +56,6 @@ val catchable_exception : exn -> bool
val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+ Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ff60ae5bf..03bc5e471 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -21,7 +21,6 @@ open Misctypes
type prim_rule =
| Cut of bool * bool * Id.t * types
| Refine of constr
- | Move of Id.t * Id.t move_location
(** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 93e276f4b..904e22681 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -123,15 +123,11 @@ let internal_cut_rev_no_check replace id t gl =
let refine_no_check c gl =
refiner (Refine c) gl
-let move_hyp_no_check id1 id2 gl =
- refiner (Move (id1,id2)) gl
-
(* Versions with consistency checks *)
let internal_cut b d t = with_check (internal_cut_no_check b d t)
let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
let refine c = with_check (refine_no_check c)
-let move_hyp id id' = with_check (move_hyp_no_check id id')
(* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 100ed1522..727efcf6d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,7 +92,6 @@ val refine_no_check : constr -> tactic
val internal_cut : bool -> Id.t -> types -> tactic
val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
-val move_hyp : Id.t -> Id.t move_location -> tactic
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : goal sigma -> Pp.std_ppcmds
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 49c91aa46..5d4350126 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -316,7 +316,18 @@ let apply_clear_request clear_flag dft c =
else Tacticals.New.tclIDTAC
(* Moving hypotheses *)
-let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
+let move_hyp id dest =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let ty = Proofview.Goal.raw_concl gl in
+ let store = Proofview.Goal.extra gl in
+ let sign = named_context_val env in
+ let sign' = move_hyp_in_named_context id dest sign in
+ let env = reset_with_named_context sign' env in
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Evarutil.new_evar env sigma ~principal:true ~store ty
+ end }
+ end }
(* Renaming hypotheses *)
let rename_hyp repl =
@@ -368,7 +379,7 @@ let rename_hyp repl =
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~unsafe:true { run = begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~store instance
+ Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
end }
end }
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 000000000..14af2d91d
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,45 @@
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Goal True.
+ idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
+Abort.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+ idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v
new file mode 100644
index 000000000..3ded4dd30
--- /dev/null
+++ b/test-suite/bugs/closed/5093.v
@@ -0,0 +1,11 @@
+Axiom P : nat -> Prop.
+Axiom PS : forall n, P n -> P (S n).
+Axiom P0 : P 0.
+
+Hint Resolve PS : foobar.
+Hint Resolve P0 : foobar.
+
+Goal P 100.
+Proof.
+Fail typeclasses eauto 100 with foobar.
+typeclasses eauto 101 with foobar.
diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v
new file mode 100644
index 000000000..20a537ab3
--- /dev/null
+++ b/test-suite/bugs/closed/5096.v
@@ -0,0 +1,219 @@
+Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
+
+Set Asymmetric Patterns.
+
+Notation eta x := (fst x, snd x).
+
+Inductive expr {var : Type} : Type :=
+| Const : expr
+| LetIn : expr -> (var -> expr) -> expr.
+
+Definition Expr := forall var, @expr var.
+
+Fixpoint count_binders (e : @expr unit) : nat :=
+match e with
+| LetIn _ eC => 1 + @count_binders (eC tt)
+| _ => 0
+end.
+
+Definition CountBinders (e : Expr) : nat := count_binders (e _).
+
+Class Context (Name : Type) (var : Type) :=
+ { ContextT : Type;
+ extendb : ContextT -> Name -> var -> ContextT;
+ empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _}, {_ _} _.
+Arguments extendb {_ _ _} _ _ _.
+Arguments empty {_ _ _}.
+
+Module Export Named.
+Inductive expr Name : Type :=
+| Const : expr Name
+| LetIn : Name -> expr Name -> expr Name -> expr Name.
+End Named.
+
+Global Arguments Const {_}.
+Global Arguments LetIn {_} _ _ _.
+
+Definition split_onames {Name : Type} (ls : list (option Name))
+ : option (Name) * list (option Name)
+ := match ls with
+ | cons n ls'
+ => (n, ls')
+ | nil => (None, nil)
+ end.
+
+Section internal.
+ Context (InName OutName : Type)
+ {InContext : Context InName (OutName)}
+ {ReverseContext : Context OutName (InName)}
+ (InName_beq : InName -> InName -> bool).
+
+ Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+ (e : expr InName) (new_names : list (option OutName))
+ : option (expr OutName)
+ := match e in Named.expr _ return option (expr _) with
+ | Const => Some Const
+ | LetIn n ex eC
+ => let '(n', new_names') := eta (split_onames new_names) in
+ match n', @register_reassign ctxi ctxr ex nil with
+ | Some n', Some x
+ => let ctxi := @extendb _ _ _ ctxi n n' in
+ let ctxr := @extendb _ _ _ ctxr n' n in
+ option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
+ | None, Some x
+ => let ctxi := ctxi in
+ @register_reassign ctxi ctxr eC new_names'
+ | _, None => None
+ end
+ end.
+
+End internal.
+
+Global Instance pos_context (var : Type) : Context positive var
+ := { ContextT := PositiveMap.t var;
+ extendb ctx key v := PositiveMap.add key v ctx;
+ empty := PositiveMap.empty _ }.
+
+Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
+
+Section language5.
+ Context (Name : Type).
+
+ Local Notation expr := (@Top.expr Name).
+ Local Notation nexpr := (@Named.expr Name).
+
+ Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
+ : option (nexpr)
+ := match e in @Top.expr _ return option (nexpr) with
+ | Top.Const => Some Named.Const
+ | Top.LetIn ex eC
+ => match @ocompile ex nil, split_onames ls with
+ | Some x, (Some n, ls')%core
+ => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
+ | _, _ => None
+ end
+ end.
+
+ Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
+End language5.
+
+Global Arguments compile {_} e ls.
+
+Fixpoint merge_liveness (ls1 ls2 : list unit) :=
+ match ls1, ls2 with
+ | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
+ | nil, ls | ls, nil => ls
+ end.
+
+Section internal1.
+ Context (Name : Type)
+ (OutName : Type)
+ {Context : Context Name (list unit)}.
+
+ Definition compute_livenessf_step
+ (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
+ (ctx : Context)
+ (e : expr Name) (prefix : list unit)
+ : list unit
+ := match e with
+ | Const => prefix
+ | LetIn n ex eC
+ => let lx := @compute_livenessf ctx ex prefix in
+ let lx := merge_liveness lx (prefix ++ repeat tt 1) in
+ let ctx := @extendb _ _ _ ctx n (lx) in
+ @compute_livenessf ctx eC (prefix ++ repeat tt 1)
+ end.
+
+ Fixpoint compute_liveness ctx e prefix
+ := @compute_livenessf_step (@compute_liveness) ctx e prefix.
+
+ Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
+ : list (option OutName)
+ := match ls with
+ | nil => nil
+ | cons live xs
+ => match lsn with
+ | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
+ | nil => def :: @insert_dead_names_gen def xs nil
+ end
+ end.
+ Definition insert_dead_names def (e : expr Name)
+ := insert_dead_names_gen def (compute_liveness empty e nil).
+End internal1.
+
+Global Arguments insert_dead_names {_ _ _} def e lsn.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+
+Section language7.
+ Context {Context : Context unit (positive)}.
+
+ Local Notation nexpr := (@Named.expr unit).
+
+ Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
+ : option (nexpr)
+ := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
+ match e with
+ | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
+ (fun names => register_reassign empty empty e names)
+ | None => None
+ end.
+End language7.
+
+Global Arguments CompileAndEliminateDeadCode {_} e ls.
+
+Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
+ := {| ContextT := Ctx;
+ extendb ctx n v := extendb ctx (f n) v;
+ empty := empty |}.
+
+Definition Register := Datatypes.unit.
+
+Global Instance RegisterContext {var : Type} : Context Register var
+ := ContextOn (fun _ => 1%positive) (pos_context var).
+
+Definition syntax := Named.expr Register.
+
+Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
+ := match res return match res with None => _ | _ => _ end with
+ | Some v => v
+ | None => I
+ end.
+
+Definition dummy_registers (n : nat) : list Register
+ := List.map (fun _ => tt) (seq 0 n).
+Definition DefaultRegisters (e : Expr) : list Register
+ := dummy_registers (CountBinders e).
+
+Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
+
+Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@Top.Const var).
+
+Definition compiled_syntax : Expr := fun (var : Type) =>
+(
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ slet x1 := #[ var ]# in
+ @Top.Const var).
+
+Definition v :=
+ Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
+
+Timeout 2 Eval vm_compute in v.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cf..356a67efe 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ Check fun (x : E) => match x with c => e c end.
Inductive C' : bool -> Set := c' : C' true.
Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+ given (and when the "inversion-and-dependencies-as-evars" strategy
+ is not strong enough because of a constructor with a type whose
+ pattern structure is not refined enough for it to be captured by
+ the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+ match y with
+ | F => f y H1
+ | G _ => f y H2
+ end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+ no explicit type constraint is given (and when the
+ "inversion-and-dependencies-as-evars" strategy is not strong enough
+ because of a constructor with a type whose pattern structure is not
+ refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+ match y with
+ | F => f y true H1
+ | G b => f y b H2
+ end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+ variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+ | F => f y true H1
+ | G b => f y b H2
+ end).
+Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 341be92d1..5eecdc64c 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -77,8 +77,8 @@ Coercion sig2_of_sigT2 : sigT2 >-> sig2.
(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *)
Require Coq.Lists.List.
Require Coq.Vectors.VectorDef.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
-Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope.
+Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
(** In 8.4, the statement of admitted lemmas did not depend on the section
variables. *)
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 0ddf1acde..54aeeaa11 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -21,4 +21,22 @@ Global Unset Regular Subst Tactic.
Global Unset Structural Injection.
Global Unset Shrink Abstract.
Global Unset Shrink Obligations.
-Global Set Refolding Reduction. \ No newline at end of file
+Global Set Refolding Reduction.
+
+(** In Coq 8.5, [] meant Vector, and [ ] meant list. Restore this
+ behavior, to allow user-defined [] to not override vector
+ notations. See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *)
+
+Require Coq.Lists.List.
+Require Coq.Vectors.VectorDef.
+Module Export Coq.
+Module Export Vectors.
+Module VectorDef.
+Export Coq.Vectors.VectorDef.
+Module VectorNotations.
+Export Coq.Vectors.VectorDef.VectorNotations.
+Notation "[]" := (VectorDef.nil _) : vector_scope.
+End VectorNotations.
+End VectorDef.
+End Vectors.
+End Coq.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 9886ae6a8..fc94d7e25 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -21,12 +21,12 @@ Set Implicit Arguments.
Open Scope list_scope.
-(** Standard notations for lists.
+(** Standard notations for lists.
In a special module to avoid conflicts. *)
Module ListNotations.
-Notation " [ ] " := nil (format "[ ]") : list_scope.
-Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope.
+Notation "[ ]" := nil (format "[ ]") : list_scope.
+Notation "[ x ]" := (cons x nil) : list_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.
End ListNotations.
Import ListNotations.
@@ -195,7 +195,7 @@ Section Facts.
Qed.
Theorem app_nil_r : forall l:list A, l ++ [] = l.
- Proof.
+ Proof.
induction l; simpl; f_equal; auto.
Qed.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index c69223804..f49b34075 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -30,7 +30,7 @@ Inductive t A : nat -> Type :=
|nil : t A 0
|cons : forall (h:A) (n:nat), t A n -> t A (S n).
-Local Notation "[]" := (nil _).
+Local Notation "[ ]" := (nil _) (format "[ ]").
Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
Section SCHEMES.
@@ -102,7 +102,7 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
Computational behavior of this function should be the same as
ocaml function. *)
-Definition nth {A} :=
+Definition nth {A} :=
fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
match p in Fin.t m' return t A m' -> A with
|Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
@@ -293,11 +293,12 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni
End VECTORLIST.
Module VectorNotations.
-Notation "[]" := [] : vector_scope.
+Delimit Scope vector_scope with vector.
+Notation "[ ]" := [] (format "[ ]") : vector_scope.
Notation "h :: t" := (h :: t) (at level 60, right associativity)
: vector_scope.
-Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; y ; .. ; z ] " := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
+Notation "[ x ]" := (x :: []) : vector_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
.
Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
Open Scope vector_scope.
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7ff59c471..35645c8e7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -108,7 +108,7 @@ let init_load_path () =
(* additional loadpath, given with options -Q and -R *)
List.iter
(fun (unix_path, coq_root, implicit) ->
- Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
+ Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
(List.rev !includes);
(* additional ml directories, given with option -I *)
List.iter Mltop.add_ml_dir (List.rev !ml_includes)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 18:31:36 +0000