aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml6
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--plugins/funind/merge.ml4
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extraargs.mli2
-rw-r--r--plugins/ltac/extratactics.ml44
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacinterp.ml32
-rw-r--r--plugins/ltac/tacinterp.mli5
-rw-r--r--plugins/setoid_ring/Ring_tac.v34
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrparser.mli4
17 files changed, 77 insertions, 38 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 4934b0750b..5a4c52456d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -84,7 +84,8 @@ let rec decompose_term env sigma t=
| Proj (p, c) ->
let canon_const kn = Constant.make1 (Constant.canonical kn) in
let p' = Projection.map canon_const p in
- (Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c))
+ let c = Retyping.expand_projection env sigma p' c [] in
+ decompose_term env sigma c
| _ ->
let t = Termops.strip_outer_cast sigma t in
if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
@@ -231,7 +232,8 @@ let make_prb gls depth additionnal_terms =
let build_projection intype (cstr:pconstructor) special default gls=
let open Tacmach.New in
let ci= (snd(fst cstr)) in
- let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ let sigma = project gls in
+ let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
sigma, mkLambda(Name id,intype,body)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 5ba98fb584..05194164b0 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -233,7 +233,7 @@ let extend_with_auto_hints env sigma l seq =
let print_cmap map=
let print_entry c l s=
- let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in
+ let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8555a0b226..8cf5e8442d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1492,7 +1492,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
msg
in
@@ -1507,7 +1507,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 89537ad3f6..8769f56688 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -618,7 +618,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
let constr_expr_typel =
- with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
+ with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
@@ -855,9 +855,9 @@ let make_graph (f_ref:global_reference) =
let sigma = Evd.from_env env in
let extern_body,extern_type =
with_full_print (fun () ->
- (Constrextern.extern_constr false env sigma body,
+ (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
Constrextern.extern_type false env sigma
- ((*FIXME*) c_body.const_type)
+ (EConstr.of_constr (*FIXME*) c_body.const_type)
)
)
()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 52a82b0e5e..3ae9221903 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -812,13 +812,13 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let typ = glob_constr_to_constr_expr tp in
CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
[] params in
- let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
+ let concl = Constrextern.extern_constr false (Global.env()) Evd.empty (EConstr.of_constr concl) in
let arity,_ =
List.fold_left
(fun (acc,env) decl ->
let nm = Context.Rel.Declaration.get_name decl in
let c = RelDecl.get_type decl in
- let typ = Constrextern.extern_constr false env Evd.empty c in
+ let typ = Constrextern.extern_constr false env Evd.empty (EConstr.of_constr c) in
let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 6097951330..89feea8dcf 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -249,7 +249,7 @@ END
let pr_by_arg_tac _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b06f35ddc4..00668ddc7d 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -64,7 +64,7 @@ val wit_by_arg_tac :
Geninterp.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
- (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f3f2f27e9e..b847aadf21 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac =
fail_evar = false;
expand_evars = true
} in
- let c = Pretyping.type_uconstr ~flags ist c in
+ let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
let replace_in_clause_maybe_by ist c1 c2 cl tac =
@@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c =
let flags =
{ constr_flags () with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
- let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
+ let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
let update = begin fun sigma ->
c env sigma
end in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 301943a509..5baa0d5c1d 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -48,7 +48,7 @@ let eval_uconstrs ist cs =
expand_evars = true
} in
let map c env sigma = c env sigma in
- List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
+ List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index dd24aa3dbf..104977aef3 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -20,7 +20,7 @@ let set_transparency cl b =
List.iter (fun r ->
let gr = Smartlocate.global_with_alias r in
let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
- Classes.set_typeclass_transparency ev false b) cl
+ Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 140cc33440..cb7d9b9c02 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Geninterp
open Stdarg
open Tacarg
open Libnames
-open Ppextend
+open Notation_term
open Misctypes
open Locus
open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0bf9bc7f62..1f6ebaf448 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,7 @@ open Misctypes
open Environ
open Constrexpr
open Tacexpr
-open Ppextend
+open Notation_term
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d3e625e73a..2a1e2b6829 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -689,7 +689,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
(* dest_fun, List.assoc may raise Not_found *)
let sigma, c = interp_fun ist env sigma x in
sigma, [c] in
- let sigma, l = List.fold_map try_expand_ltac_var sigma l in
+ let sigma, l = List.fold_left_map try_expand_ltac_var sigma l in
sigma, List.flatten l
let interp_constr_list ist env sigma c =
@@ -908,18 +908,18 @@ and interp_intro_pattern_action ist env sigma = function
and interp_or_and_intro_pattern ist env sigma = function
| IntroAndPattern l ->
- let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_intro_pattern ist env) sigma l in
sigma, IntroAndPattern l
| IntroOrPattern ll ->
- let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in
+ let sigma, ll = List.fold_left_map (interp_intro_pattern_list_as_list ist env) sigma ll in
sigma, IntroOrPattern ll
and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
(try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
- List.fold_map (interp_intro_pattern ist env) sigma l)
- | l -> List.fold_map (interp_intro_pattern ist env) sigma l
+ List.fold_left_map (interp_intro_pattern ist env) sigma l)
+ | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
let interp_intro_pattern_naming_option ist env sigma = function
| None -> None
@@ -973,7 +973,7 @@ let interp_bindings ist env sigma = function
let sigma, l = interp_open_constr_list ist env sigma l in
sigma, ImplicitBindings l
| ExplicitBindings l ->
- let sigma, l = List.fold_map (interp_binding ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in
sigma, ExplicitBindings l
let interp_constr_with_bindings ist env sigma (c,bl) =
@@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function
:: read_match_rule lfun ist env sigma tl
| [] -> []
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None })
+ ?(expected_type = WithoutTypeConstraint) ist c =
+ begin fun env sigma ->
+ let { closure; term } = c in
+ let vars = {
+ ltac_constrs = closure.typed;
+ ltac_uconstrs = closure.untyped;
+ ltac_idents = closure.idents;
+ ltac_genargs = Id.Map.empty;
+ } in
+ understand_ltac flags env sigma vars expected_type term
+ end
+
let warn_deprecated_info =
CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
(fun () ->
@@ -1657,7 +1671,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
- let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in
+ let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in
let named_tac =
let tac = Tactics.elim ev keep cb cbo in
name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
@@ -1775,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
- List.fold_map begin fun sigma (c,(ipato,ipats),cls) ->
+ List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) ->
(* TODO: move sigma as a side-effect *)
(* spiwack: the [*p] variants are for printing *)
let cp = c in
@@ -1789,7 +1803,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let l,lp = List.split l in
let sigma,el =
- Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in
+ Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(name_atomic ~env
(TacInductionDestruct(isrec,ev,(lp,el)))
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 73e4f3d6ab..c1ab2b4c49 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -54,6 +54,11 @@ val set_debug : debug_info -> unit
(** Gives the state of debug *)
val get_debug : unit -> debug_info
+val type_uconstr :
+ ?flags:Pretyping.inference_flags ->
+ ?expected_type:Pretyping.typing_constraint ->
+ Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+
(** Adds an interpretation function for extra generic arguments *)
val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index fc02cef100..329fa0ee81 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -427,19 +427,37 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
let t := type of H in
let g := fresh "goal" in
set (g:= G);
- generalize H;clear H;
+ generalize H;
ring_lookup (PackRing Ring_simplify) [] rl t;
- intro H;
+ (*
+ Correction of bug 1859:
+ we want to leave H at its initial position
+ this is obtained by adding a copy of H (H'),
+ move it just after H, remove H and finally
+ rename H into H'
+ *)
+ let H' := fresh "H" in
+ intro H';
+ move H' after H;
+ clear H;rename H' into H;
unfold g;clear g.
-Tactic Notation
- "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
+Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
let G := Get_goal in
let t := type of H in
let g := fresh "goal" in
set (g:= G);
- generalize H;clear H;
+ generalize H;
ring_lookup (PackRing Ring_simplify) [lH] rl t;
- intro H;
- unfold g;clear g.
-
+ (*
+ Correction of bug 1859:
+ we want to leave H at its initial position
+ this is obtained by adding a copy of H (H'),
+ move it just after H, remove H and finally
+ rename H into H'
+ *)
+ let H' := fresh "H" in
+ intro H';
+ move H' after H;
+ clear H;rename H' into H;
+ unfold g;clear g. \ No newline at end of file
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index ce23bb2b30..db1981228a 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -62,7 +62,7 @@ DECLARE PLUGIN "ssreflect_plugin"
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
-let tacltop = (5,Ppextend.E)
+let tacltop = (5,Notation_term.E)
let pr_ssrtacarg _ _ prt = prt tacltop
ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 88beeaa711..f9dc345e15 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -10,11 +10,11 @@
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:36:14 +0000