aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh6
-rw-r--r--dev/include_printers1
-rw-r--r--dev/top_printers.dbg1
-rw-r--r--dev/top_printers.ml10
-rw-r--r--dev/top_printers.mli1
-rw-r--r--pretyping/detyping.ml13
-rw-r--r--pretyping/detyping.mli3
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tactics.ml152
-rw-r--r--tactics/tactics.mli1
-rw-r--r--test-suite/bugs/closed/bug_10026.v3
-rw-r--r--test-suite/bugs/closed/bug_3754.v (renamed from test-suite/bugs/opened/bug_3754.v)4
-rw-r--r--user-contrib/Ltac2/Constr.v1
-rw-r--r--user-contrib/Ltac2/Init.v1
-rw-r--r--user-contrib/Ltac2/tac2core.ml7
-rw-r--r--user-contrib/Ltac2/tac2ffi.ml23
-rw-r--r--user-contrib/Ltac2/tac2ffi.mli6
17 files changed, 122 insertions, 113 deletions
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
new file mode 100644
index 0000000000..bc8aa33565
--- /dev/null
+++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
+
+ unicoq_CI_REF=detype-anonymous
+ unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+fi
diff --git a/dev/include_printers b/dev/include_printers
index 90088e40bf..d077075eeb 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -11,6 +11,7 @@
#install_printer (* universes *) ppuniverses;;
#install_printer (* univ level *) ppuni_level;;
#install_printer (* univ context *) ppuniverse_context;;
+#install_printer (* univ context *) ppaucontext;;
#install_printer (* univ context future *) ppuniverse_context_future;;
#install_printer (* univ context set *) ppuniverse_context_set;;
#install_printer (* univ set *) ppuniverse_set;;
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index a6ecec7e33..82f2e79549 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level
install_printer Top_printers.ppuniverse_set
install_printer Top_printers.ppuniverse_instance
install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppaucontext
install_printer Top_printers.ppuniverse_context_set
install_printer Top_printers.ppuniverse_subst
install_printer Top_printers.ppuniverse_opt_subst
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..2859b56cbe 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,7 +27,6 @@ open Clenv
let _ = Detyping.print_evar_arguments := true
let _ = Detyping.print_universes := true
let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
(* std_ppcmds *)
let pp x = Pp.pp_with !Topfmt.std_ft x
@@ -236,6 +235,15 @@ let ppnamedcontextval e =
let sigma = Evd.from_env env in
pp (pr_named_context env sigma (named_context_of_val e))
+let ppaucontext auctx =
+ let nas = AUContext.names auctx in
+ let prlev l = match Level.var_index l with
+ | Some n -> Name.print nas.(n)
+ | None -> prlev l
+ in
+ pp (pr_universe_context prlev (AUContext.repr auctx))
+
+
let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index cb32d2294c..2aa1808322 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
val ppuniverse_set : Univ.LSet.t -> unit
val ppuniverse_instance : Univ.Instance.t -> unit
val ppuniverse_context : Univ.UContext.t -> unit
+val ppaucontext : Univ.AUContext.t -> unit
val ppuniverse_context_set : Univ.ContextSet.t -> unit
val ppuniverse_subst : Univ.universe_subst -> unit
val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 062e3ca8b2..82726eccf0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn
(**********************************************************************)
(* Main detyping function *)
-let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable."))
-let set_detype_anonymous f = detype_anonymous := f
-
let detype_level sigma l =
let l = hack_qualid_of_univ_level sigma l in
GType (UNamed l)
@@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t =
match EConstr.kind sigma (collapse_appl sigma t) with
| Rel n ->
(try match lookup_name_of_rel n (fst env) with
- | Name id -> GVar id
- | Anonymous -> GVar (!detype_anonymous n)
+ | Name id -> GVar id
+ | Anonymous ->
+ let s = "_ANONYMOUS_REL_"^(string_of_int n) in
+ GVar (Id.of_string s)
with Not_found ->
- let s = "_UNBOUND_REL_"^(string_of_int n)
- in GVar (Id.of_string s))
+ let s = "_UNBOUND_REL_"^(string_of_int n)
+ in GVar (Id.of_string s))
| Meta n ->
(* Meta in constr are not user-parsable and are mapped to Evar *)
if n = Constr_matching.special_meta then
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 1a8e97efb8..00b0578a52 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo
val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option
val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
-(* XXX: This is a hack and should go away *)
-val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit
-
val force_wildcard : unit -> bool
val synthetize_type : unit -> bool
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f049f8c568..45a4799ea1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
- {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
+ {elimindex = None; elimbody = (elim,NoBindings) }
end
let adjust_rewriting_direction args lft2rgt =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 806c955591..2bdfc85d6d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1302,14 +1302,11 @@ let do_replace id = function
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
- targetid id sigma0 clenv tac =
+let clenv_refine_in with_evars targetid id sigma0 clenv tac =
let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
- if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses
~fail:(not with_evars) clenv.env clenv.evd }
- else clenv
in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
@@ -1321,11 +1318,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
- (if sidecond_first then
- Tacticals.New.tclTHENFIRST
- (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
- else
- Tacticals.New.tclTHENLAST
+ (Tacticals.New.tclTHENLAST
(assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
(********************************************)
@@ -1360,22 +1353,25 @@ let rec contract_letin_in_lam_header sigma c =
| LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c)
| _ -> c
-let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ())
- rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let elim = contract_letin_in_lam_header sigma elim in
- let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
- let indmv =
- (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
- | Meta mv -> mv
- | _ -> user_err ~hdr:"elimination_clause"
- (str "The type of elimination clause is not well-formed."))
+let elimination_in_clause_scheme env sigma with_evars ~flags
+ id hypmv elimclause =
+ let hyp = mkVar id in
+ let hyp_typ = Retyping.get_type_of env sigma hyp in
+ let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
+ let elimclause'' =
+ (* The evarmap of elimclause is assumed to be an extension of hypclause, so
+ we do not need to merge the universes coming from hypclause. *)
+ try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause
+ with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
+ (* Set the hypothesis name in the message *)
+ raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
in
- let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
- end
+ let new_hyp_typ = clenv_type elimclause'' in
+ if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
+ user_err ~hdr:"general_rewrite_in"
+ (str "Nothing to rewrite in " ++ Id.print id ++ str".");
+ clenv_refine_in with_evars id id sigma elimclause''
+ (fun id -> Proofview.tclUNIT ())
(*
* Elimination tactic with bindings and using an arbitrary
@@ -1387,11 +1383,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
type eliminator = {
elimindex : int option; (* None = find it automatically *)
- elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
elimbody : EConstr.constr with_bindings
}
-let general_elim_clause_gen elimtac indclause elim =
+let general_elim_clause with_evars flags where indclause elim =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -1399,7 +1394,27 @@ let general_elim_clause_gen elimtac indclause elim =
let elimt = Retyping.get_type_of env sigma elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
- elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
+ let elimc = contract_letin_in_lam_header sigma elimc in
+ let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in
+ let indmv =
+ (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
+ | Meta mv -> mv
+ | _ -> user_err ~hdr:"elimination_clause"
+ (str "The type of elimination clause is not well-formed."))
+ in
+ match where with
+ | None ->
+ let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+ Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags
+ | Some id ->
+ let hypmv =
+ match List.remove Int.equal indmv (clenv_independent elimclause) with
+ | [a] -> a
+ | _ -> user_err ~hdr:"elimination_clause"
+ (str "The type of elimination clause is not well-formed.")
+ in
+ let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+ elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause
end
let general_elim with_evars clear_flag (c, lbindc) elim =
@@ -1408,12 +1423,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
let sigma = Tacmach.New.project gl in
let ct = Retyping.get_type_of env sigma c in
let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
- let elimtac = elimination_clause_scheme with_evars in
let indclause = make_clenv_binding env sigma (c, t) lbindc in
let sigma = meta_merge sigma (clear_metas indclause.evd) in
+ let flags = elim_flags () in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.New.tclTHEN
- (general_elim_clause_gen elimtac indclause elim)
+ (general_elim_clause with_evars flags None indclause elim)
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
end
@@ -1436,8 +1451,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
let elim = EConstr.of_constr elim in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(general_elim with_evars clear_flag (c,lbindc)
- {elimindex = None; elimbody = (elim,NoBindings);
- elimrename = Some (false, constructors_nrealdecls env (fst mind))})
+ {elimindex = None; elimbody = (elim,NoBindings); })
end
let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1468,8 +1482,7 @@ let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
if is_nonrec ind then raise IsNonrec;
let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
- evd, {elimindex = None; elimbody = (c,NoBindings);
- elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)}
+ evd, { elimindex = None; elimbody = (c,NoBindings) }
let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
@@ -1489,7 +1502,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
let elim_in_context with_evars clear_flag c = function
| Some elim ->
general_elim with_evars clear_flag c
- {elimindex = Some (-1); elimbody = elim; elimrename = None}
+ { elimindex = Some (-1); elimbody = elim }
| None -> default_elim with_evars clear_flag c
let elim with_evars clear_flag (c,lbindc as cx) elim =
@@ -1515,48 +1528,6 @@ let simplest_elim c = default_elim false None (c,NoBindings)
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
-let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
- (* The evarmap of elimclause is assumed to be an extension of hypclause, so
- we do not need to merge the universes coming from hypclause. *)
- try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
- with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
- (* Set the hypothesis name in the message *)
- raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
- id rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let elim = contract_letin_in_lam_header sigma elim in
- let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
- let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
- let hypmv =
- match List.remove Int.equal indmv (clenv_independent elimclause) with
- | [a] -> a
- | _ -> user_err ~hdr:"elimination_clause"
- (str "The type of elimination clause is not well-formed.")
- in
- let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- let hyp = mkVar id in
- let hyp_typ = Retyping.get_type_of env sigma hyp in
- let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
- let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
- let new_hyp_typ = clenv_type elimclause'' in
- if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
- user_err ~hdr:"general_rewrite_in"
- (str "Nothing to rewrite in " ++ Id.print id ++ str".");
- clenv_refine_in with_evars id id sigma elimclause''
- (fun id -> Proofview.tclUNIT ())
- end
-
-let general_elim_clause with_evars flags id c e =
- let elim = match id with
- | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags
- | Some id -> elimination_in_clause_scheme with_evars ~flags id
- in
- general_elim_clause_gen elim c e
-
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
@@ -1828,7 +1799,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
in
aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_once ?(respect_opaque = false) with_delta
with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
@@ -1849,7 +1820,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
- clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
+ clenv_refine_in with_evars targetid id sigma clause
(fun id ->
Tacticals.New.tclTHENLIST [
apply_clear_request clear_flag false c;
@@ -1866,14 +1837,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
aux [] with_destruct d
end
-let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_delayed_once ?(respect_opaque = false) with_delta
with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
- (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
+ (apply_in_once ~respect_opaque with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
end
@@ -2493,7 +2464,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
clear [id] in
let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
in
- apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f)
+ apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f)
(fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
and prepare_intros ?loc with_evars dft destopt = function
@@ -2561,10 +2532,10 @@ let assert_as first hd ipat t =
(* apply in as *)
-let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+let general_apply_in ?(respect_opaque=false) with_delta
with_destruct with_evars id lemmas ipat =
let tac (naming,lemma) tac id =
- apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+ apply_in_delayed_once ~respect_opaque with_delta
with_destruct with_evars naming id lemma tac in
Proofview.Goal.enter begin fun gl ->
let destopt =
@@ -2593,10 +2564,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
let apply_in simple with_evars id lemmas ipat =
let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
- general_apply_in false simple simple with_evars id lemmas ipat
+ general_apply_in simple simple with_evars id lemmas ipat
let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
+ general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
@@ -4183,7 +4154,7 @@ let find_induction_type isrec elim hyp0 gl =
let scheme = compute_elim_sig sigma ~elimc elimt in
if Option.is_empty scheme.indarg then error "Cannot find induction type";
let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
- let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
+ let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
scheme, ElimUsing (elim,indsign)
in
match scheme.indref with
@@ -4210,10 +4181,7 @@ let get_eliminator elim dep s gl =
| ElimOver (isrec,id) ->
let evd, (elimc,elimt),_ as elims = guess_elim isrec 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)
- in
- evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
+ evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l
(* Instantiate all meta variables of elimclause using lid, some elts
of lid are parameters (first ones), the other are
@@ -4257,7 +4225,7 @@ let recolle_clenv i params args elimclause gl =
let induction_tac with_evars params indvars elim =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
- let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
+ let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in
let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
let elimc = contract_letin_in_lam_header sigma elimc in
@@ -4362,7 +4330,7 @@ let induction_without_atomization isrec with_evars elim names lid =
(* FIXME: Tester ca avec un principe dependant et non-dependant *)
induction_tac with_evars params realindvars elim;
] in
- let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
+ let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in
apply_induction_in_context with_evars None [] elim indvars names induct_tac
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9eb8196280..32c64bacf6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_
(** elim principle with the index of its inductive arg *)
type eliminator = {
elimindex : int option; (** None = find it automatically *)
- elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
elimbody : constr with_bindings
}
diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v
new file mode 100644
index 0000000000..0d3142d0f2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10026.v
@@ -0,0 +1,3 @@
+Require Import Coq.Lists.List.
+Set Debug RAKAM.
+Check fun _ => fold_right (fun A B => prod A B) unit _.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v
index 18820b1a4c..7031cbf132 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/closed/bug_3754.v
@@ -281,5 +281,7 @@ Defined.
(factor2 fact)).
rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
Set Debug Tactic Unification.
- Fail rewrite (concat_Ap ff2).
+ rewrite (concat_Ap ff2).
Abort.
+
+End Factorization.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index d8d222730e..1701bf4365 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -38,6 +38,7 @@ Ltac2 Type kind := [
| Fix (int array, int, ident option array, constr array, constr array)
| CoFix (int, ident option array, constr array, constr array)
| Proj (projection, constr)
+| Uint63 (uint63)
].
Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind".
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 16e7d7a6f9..dc1690bdfb 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -14,6 +14,7 @@ Ltac2 Type int.
Ltac2 Type string.
Ltac2 Type char.
Ltac2 Type ident.
+Ltac2 Type uint63.
(** Constr-specific built-in types *)
Ltac2 Type meta.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index d7e7b91ee6..da8600109e 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -424,8 +424,8 @@ let () = define1 "constr_kind" constr begin fun c ->
Value.of_ext Value.val_projection p;
Value.of_constr c;
|]
- | Int _ ->
- assert false
+ | Int n ->
+ v_blk 17 [|Value.of_uint63 n|]
end
end
@@ -503,6 +503,9 @@ let () = define1 "constr_make" valexpr begin fun knd ->
let p = Value.to_ext Value.val_projection p in
let c = Value.to_constr c in
EConstr.mkProj (p, c)
+ | (17, [|n|]) ->
+ let n = Value.to_uint63 n in
+ EConstr.mkInt n
| _ -> assert false
in
return (Value.of_constr c)
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index e3127ab9df..1043d25a75 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -30,6 +30,8 @@ type valexpr =
(** Open constructors *)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
+| ValUint63 of Uint63.t
+ (** Primitive integers *)
and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure
@@ -47,21 +49,21 @@ type t = valexpr
let is_int = function
| ValInt _ -> true
-| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false
+| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false
let tag v = match v with
| ValBlk (n, _) -> n
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let field v n = match v with
| ValBlk (_, v) -> v.(n)
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let set_field v n w = match v with
| ValBlk (_, v) -> v.(n) <- w
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ ->
CErrors.anomaly (Pp.str "Unexpected value shape")
let make_block tag v = ValBlk (tag, v)
@@ -192,7 +194,7 @@ let of_closure cls = ValCls cls
let to_closure = function
| ValCls cls -> cls
-| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false
let closure = {
r_of = of_closure;
@@ -318,6 +320,17 @@ let open_ = {
r_id = false;
}
+let of_uint63 n = ValUint63 n
+let to_uint63 = function
+| ValUint63 n -> n
+| _ -> assert false
+
+let uint63 = {
+ r_of = of_uint63;
+ r_to = to_uint63;
+ r_id = false;
+}
+
let of_constant c = of_ext val_constant c
let to_constant c = to_ext val_constant c
let constant = repr_ext val_constant
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index bfc93d99e6..f8581061a0 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -28,6 +28,8 @@ type valexpr =
(** Open constructors *)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
+| ValUint63 of Uint63.t
+ (** Primitive integers *)
type 'a arity
@@ -143,6 +145,10 @@ val of_open : KerName.t * valexpr array -> valexpr
val to_open : valexpr -> KerName.t * valexpr array
val open_ : (KerName.t * valexpr array) repr
+val of_uint63 : Uint63.t -> valexpr
+val to_uint63 : valexpr -> Uint63.t
+val uint63 : Uint63.t repr
+
type ('a, 'b) fun1
val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:30:59 +0000