aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/mlutil.ml6
-rw-r--r--plugins/ltac/coretactics.mlg8
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_auto.mlg20
-rw-r--r--plugins/ltac/g_class.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg4
-rw-r--r--plugins/ltac/g_tactic.mlg16
-rw-r--r--plugins/ltac/pltac.ml2
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/rewrite.ml19
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml9
-rw-r--r--plugins/ltac/tacinterp.ml9
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--plugins/micromega/coq_micromega.ml6
-rw-r--r--plugins/micromega/g_micromega.mlg6
-rw-r--r--plugins/micromega/persistent_cache.ml148
-rw-r--r--plugins/ring/ring.ml288
-rw-r--r--plugins/ssr/ssrparser.mlg2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--plugins/ssrsearch/g_search.mlg2
23 files changed, 333 insertions, 240 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 21ec80abbc..da4a50b674 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
| MLuint i1, MLuint i2 -> Uint63.equal i1 i2
| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
-| _, _ -> false
+| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2
+| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _
+ |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom
+ | MLmagic _| MLuint _| MLfloat _|MLparray _), _
+ -> false
and eq_ml_pattern p1 p2 = match p1, p2 with
| Pcons (gr1, p1), Pcons (gr2, p2) ->
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index b7ac71181a..e39c066c95 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -122,10 +122,10 @@ END
TACTIC EXTEND constructor
| [ "constructor" ] -> { Tactics.any_constructor false None }
-| [ "constructor" int_or_var(i) ] -> {
+| [ "constructor" nat_or_var(i) ] -> {
Tactics.constructor_tac false None i NoBindings
}
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "constructor" nat_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac false None i bl in
Tacticals.New.tclDELAYEDWITHHOLES false bl tac
}
@@ -133,10 +133,10 @@ END
TACTIC EXTEND econstructor
| [ "econstructor" ] -> { Tactics.any_constructor true None }
-| [ "econstructor" int_or_var(i) ] -> {
+| [ "econstructor" nat_or_var(i) ] -> {
Tactics.constructor_tac true None i NoBindings
}
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "econstructor" nat_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac true None i bl in
Tacticals.New.tclDELAYEDWITHHOLES true bl tac
}
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index a2a47c0bf4..6ab82b1253 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -686,7 +686,7 @@ let hResolve_auto id c t =
}
TACTIC EXTEND hresolve_core
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t }
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" nat_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t }
| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t }
END
@@ -695,7 +695,7 @@ END
*)
TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n }
+| [ "hget_evar" nat_or_var(n) ] -> { Evar_tactics.hget_evar n }
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7e8400910c..eed9419946 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -96,17 +96,17 @@ TACTIC EXTEND debug_trivial
END
TACTIC EXTEND auto
-| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_auto
-| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "info_auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND debug_auto
-| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "debug" "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db }
END
@@ -130,15 +130,15 @@ let deprecated_bfs tacname =
}
TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
-TACTIC EXTEND new_eauto
-| [ "new" "auto" int_or_var_opt(n) auto_using(lems)
+TACTIC EXTEND new_eauto (* todo: name doesn't match syntax *)
+| [ "new" "auto" nat_or_var_opt(n) auto_using(lems)
hintbases(db) ] ->
{ match db with
| None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems)
@@ -146,7 +146,7 @@ TACTIC EXTEND new_eauto
END
TACTIC EXTEND debug_eauto
-| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "debug" "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
@@ -154,7 +154,7 @@ TACTIC EXTEND debug_eauto
END
TACTIC EXTEND info_eauto
-| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "info_eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{
( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
@@ -162,13 +162,13 @@ TACTIC EXTEND info_eauto
END
TACTIC EXTEND dfs_eauto
-| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "dfs" "eauto" nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND bfs_eauto
-| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "bfs" "eauto" nat_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
{ Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
END
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8c2e633be5..0f59ac07b4 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -86,13 +86,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d ~strategy:Bfs l }
- | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
- | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) ] -> {
typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c2e95c45f9..b1b96ea9a7 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -112,8 +112,8 @@ GRAMMAR EXTEND Gram
| true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
[ IDENT "try"; ta = ltac_expr -> { TacTry ta }
- | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
- | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+ | IDENT "do"; n = nat_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+ | IDENT "timeout"; n = nat_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
| IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
| IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
| IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 236de65462..43957bbde5 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -190,7 +190,7 @@ open Pvernac.Vernac_
GRAMMAR EXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
- bindings red_expr int_or_var open_constr uconstr
+ bindings red_expr int_or_var nat_or_var open_constr uconstr
simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
int_or_var:
@@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
- | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
- (* have used int_or_var instead of nat_or_var for compatibility *)
- { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
+ | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
@@ -379,9 +377,11 @@ GRAMMAR EXTEND Gram
{ {onhyps=None; concl_occs=occs} }
| "*"; "|-"; occs=concl_occ ->
{ {onhyps=None; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
+ | "|-"; occs=concl_occ ->
+ { {onhyps=Some []; concl_occs=occs} }
+ | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ ->
{ {onhyps=Some hl; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP"," ->
+ | hl = LIST1 hypident_occ SEP "," ->
{ {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
;
clause_dft_concl:
@@ -407,8 +407,8 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
- | -> { None } ] ]
+ [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
+ | -> { [] } ] ]
;
orient_rw:
[ [ "->" -> { true }
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 94e398fe5d..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -29,6 +29,7 @@ let quantified_hypothesis =
Entry.create "quantified_hypothesis"
let destruction_arg = Entry.create "destruction_arg"
let int_or_var = Entry.create "int_or_var"
+let nat_or_var = Entry.create "nat_or_var"
let simple_intropattern =
Entry.create "simple_intropattern"
let in_clause = Entry.create "in_clause"
@@ -52,6 +53,7 @@ let () =
let open Stdarg in
let open Tacarg in
register_grammar wit_int_or_var (int_or_var);
+ register_grammar wit_nat_or_var (nat_or_var);
register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *)
(* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *)
register_grammar wit_simple_intropattern (simple_intropattern);
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 3a4a081c93..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -27,6 +27,7 @@ val uconstr : constr_expr Entry.t
val quantified_hypothesis : quantified_hypothesis Entry.t
val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
val int_or_var : int Locus.or_var Entry.t
+val nat_or_var : int Locus.or_var Entry.t
val simple_tactic : raw_tactic_expr Entry.t
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
val in_clause : Names.lident Locus.clause_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index edd56ee0f7..cd7b1f7f28 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -458,8 +458,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
let pr_in_hyp_as prc pr_id = function
- | None -> mt ()
- | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+ | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
let pr_in_clause pr_id = function
| { onhyps=None; concl_occs=NoOccurrences } ->
@@ -756,7 +755,7 @@ let pr_goal_selector ~toplevel s =
(if a then mt() else primitive "simple ") ++
primitive (with_evars ev "apply") ++ spc () ++
prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+ prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
)
| TacElim (ev,cb,cbo) ->
hov 1 (
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26e2b18a02..77162ce89a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Nameops
-open Namegen
open Constr
open Context
open EConstr
@@ -485,7 +484,7 @@ let rec decompose_app_rel env evd t =
let (f', argl, argr) = decompose_app_rel env evd arg in
let ty = Retyping.get_type_of env evd argl in
let r = Retyping.relevance_of_type env evd ty in
- let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
+ let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty,
mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
in (f'', argl, argr)
@@ -1119,7 +1118,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
*)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh, n' =
+ let id = match n.binder_name with
+ | Anonymous -> Namegen.default_dependent_ident
+ | Name id -> id
+ in
+ let id = Tactics.fresh_id_in_env unfresh id env in
+ Id.Set.add id unfresh, {n with binder_name = Name id}
+ in
let unfresh = match n'.binder_name with
| Anonymous -> unfresh
| Name id -> Id.Set.add id unfresh
@@ -1542,7 +1548,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
(* For compatibility *)
let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
- let treat sigma res =
+ let treat sigma res state =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None ->
@@ -1553,7 +1559,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- let gls = List.map Proofview.with_empty_state gls in
+ let gls = List.map (fun gl -> Proofview.goal_with_state gl state) gls in
match clause, prf with
| Some id, Some p ->
let tac = tclTHENLIST [
@@ -1583,6 +1589,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
+ let state = Proofview.Goal.state gl in
let sigma = Tacmach.New.project gl in
let ty = match clause with
| None -> concl
@@ -1602,7 +1609,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
- treat sigma res <*>
+ treat sigma res state <*>
(* For compatibility *)
beta <*> Proofview.shelve_unifiable
with
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index eaedf8d9c1..7b2c8e1d04 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -108,7 +108,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 50767821e4..2382dcfbb9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -107,7 +107,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 47f1d3bf66..8bee7afa2c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -444,11 +444,11 @@ let intern_red_expr ist = function
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
-let intern_in_hyp_as ist lf (id,ipat) =
- (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
let intern_hyp_list ist = List.map (intern_hyp ist)
+let intern_in_hyp_as ist lf (idl,ipat) =
+ (intern_hyp ist idl, Option.map (intern_intro_pattern lf ist) ipat)
+
let intern_inversion_strength lf ist = function
| NonDepInversion (k,idl,ids) ->
NonDepInversion (k,intern_hyp_list ist idl,
@@ -527,7 +527,7 @@ let rec intern_atomic lf ist x =
TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
| TacApply (a,ev,cb,inhyp) ->
TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
- Option.map (intern_in_hyp_as ist lf) inhyp)
+ List.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings_arg ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
@@ -799,6 +799,7 @@ let intern_ltac ist tac =
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+ Genintern.register_intern0 wit_nat_or_var (lift intern_int_or_var);
Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3d734d3a66..00ac155f0e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
(k,(make ?loc f))) cb
in
let sigma,tac = match cl with
- | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
- | Some cl ->
- let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
- sigma, Tactics.apply_delayed_in a ev id l cl in
+ | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
+ | cl ->
+ let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in
+ sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in
Tacticals.New.tclWITHHOLES ev tac sigma
end
end
@@ -2099,6 +2099,7 @@ let interp_pre_ident ist env sigma s =
let () =
register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+ register_interp0 wit_nat_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
register_interp0 wit_smart_global (lift interp_reference);
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ec44ae4698..90546ea939 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -128,7 +128,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Basic tactics *)
| TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
| TacApply (a,ev,cb,cl) ->
- TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
+ TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,
+ List.map (on_snd (Option.map (subst_intro_pattern subst))) cl)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_glob_with_bindings_arg subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
@@ -278,6 +279,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
let () =
Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
+ Genintern.register_subst0 wit_nat_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 08edd1fc5e..e119ceb241 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2075,7 +2075,11 @@ module MakeCache (T : sig
val hash_coeff : int -> coeff -> int
val eq_prover_option : prover_option -> prover_option -> bool
val eq_coeff : coeff -> coeff -> bool
-end) =
+end) :
+sig
+ type key = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
+ val memo_opt : (unit -> bool) -> string -> (key -> 'a) -> key -> 'a
+end =
struct
module E = struct
type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg
index 40eea91b31..852a485329 100644
--- a/plugins/micromega/g_micromega.mlg
+++ b/plugins/micromega/g_micromega.mlg
@@ -29,7 +29,7 @@ open Tacarg
DECLARE PLUGIN "micromega_plugin"
TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
+| [ "psatz_Z" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
(Tacinterp.tactic_of_value ist t))
}
| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
@@ -74,12 +74,12 @@ TACTIC EXTEND LRA_R
END
TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" nat_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
END
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 21178a64a5..6e997696cb 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -33,11 +33,32 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
type key = Key.t
- module Table = Hashtbl.Make (Key)
-
- exception InvalidTableFormat
-
- type 'a t = {outch : out_channel; htbl : 'a Table.t}
+ module Table :
+ sig
+ type 'a t
+ val empty : 'a t
+ val add : int -> 'a -> 'a t -> 'a t
+ val find : int -> 'a t -> 'a list
+ val fold : (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+ end =
+ struct
+ type 'a t = 'a list Int.Map.t
+ let empty = Int.Map.empty
+ let add h pos tab =
+ try Int.Map.modify h (fun _ l -> pos :: l) tab
+ with Not_found -> Int.Map.add h [pos] tab
+
+ let fold f tab accu =
+ let fold h l accu = List.fold_left (fun accu pos -> f h pos accu) accu l in
+ Int.Map.fold fold tab accu
+
+ let find h tab = Int.Map.find h tab
+ end
+ (* A mapping key hash -> file position *)
+
+ type 'a data = { pos : int; mutable obj : (Key.t * 'a) option }
+
+ type 'a t = {outch : out_channel; mutable htbl : 'a data Table.t; file : string }
(* XXX: Move to Fun.protect once in Ocaml 4.08 *)
let fun_protect ~(finally : unit -> unit) work =
@@ -55,10 +76,19 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
finally_no_exn ();
Printexc.raise_with_backtrace work_exn work_bt
- let read_key_elem inch =
- try Some (Marshal.from_channel inch) with
- | End_of_file -> None
- | e when CErrors.noncritical e -> raise InvalidTableFormat
+ let skip_blob ch =
+ let hd = Bytes.create Marshal.header_size in
+ let () = really_input ch hd 0 Marshal.header_size in
+ let len = Marshal.data_size hd 0 in
+ let pos = pos_in ch in
+ seek_in ch (pos + len)
+
+ let read_key_elem inch = match input_binary_int inch with
+ | hash ->
+ let pos = pos_in inch in
+ let () = skip_blob inch in
+ Some (hash, pos)
+ | exception End_of_file -> None
(**
We used to only lock/unlock regions.
@@ -100,48 +130,98 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
let do_under_lock kd fd f =
if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f ()
- let open_in f =
+ let fopen_in = open_in
+
+ let open_in (type a) f : a t =
let flags = [O_RDONLY; O_CREAT] in
let finch = openfile f flags 0o666 in
let inch = in_channel_of_descr finch in
- let htbl = Table.create 100 in
- let rec xload () =
+ let exception InvalidTableFormat of a data Table.t in
+ let rec xload table =
match read_key_elem inch with
- | None -> ()
- | Some (key, elem) -> Table.add htbl key elem; xload ()
+ | None -> table
+ | Some (hash, pos) -> xload (Table.add hash { pos; obj = None } table)
+ | exception e when CErrors.noncritical e -> raise (InvalidTableFormat table)
in
try
(* Locking of the (whole) file while reading *)
- do_under_lock Read finch xload;
- close_in_noerr inch;
- { outch =
- out_channel_of_descr (openfile f [O_WRONLY; O_APPEND; O_CREAT] 0o666)
- ; htbl }
- with InvalidTableFormat ->
+ let htbl = do_under_lock Read finch (fun () -> xload Table.empty) in
+ let () = close_in_noerr inch in
+ let outch = out_channel_of_descr (openfile f [O_WRONLY; O_APPEND; O_CREAT] 0o666) in
+ { outch ; file = f; htbl }
+ with InvalidTableFormat htbl ->
(* The file is corrupted *)
- close_in_noerr inch;
+ let fold hash data accu =
+ let () = seek_in inch data.pos in
+ match Marshal.from_channel inch with
+ | (k, v) -> (hash, k, v) :: accu
+ | exception e -> accu
+ in
+ (* Try to salvage what we can *)
+ let data = do_under_lock Read finch (fun () -> Table.fold fold htbl []) in
+ let () = close_in_noerr inch in
let flags = [O_WRONLY; O_TRUNC; O_CREAT] in
let out = openfile f flags 0o666 in
let outch = out_channel_of_descr out in
- do_under_lock Write out (fun () ->
- Table.iter
- (fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing])
- htbl;
- flush outch);
- {outch; htbl}
+ let fold htbl (h, k, e) =
+ let () = output_binary_int outch h in
+ let pos = pos_out outch in
+ let () = Marshal.to_channel outch (k, e) [] in
+ Table.add h { pos; obj = None } htbl
+ in
+ let dump () =
+ let htbl = List.fold_left fold Table.empty data in
+ let () = flush outch in
+ htbl
+ in
+ let htbl = do_under_lock Write out dump in
+ {outch; htbl; file = f}
let add t k e =
- let {outch; htbl = tbl} = t in
+ let {outch} = t in
let fd = descr_of_out_channel outch in
- Table.add tbl k e;
- do_under_lock Write fd (fun _ ->
- Marshal.to_channel outch (k, e) [Marshal.No_sharing];
- flush outch)
+ let h = Key.hash k land 0x7FFFFFFF in
+ let dump () =
+ let () = output_binary_int outch h in
+ let pos = pos_out outch in
+ let () = Marshal.to_channel outch (k, e) [] in
+ let () = flush outch in
+ pos
+ in
+ let pos = do_under_lock Write fd dump in
+ t.htbl <- Table.add h { pos; obj = Some (k, e) } t.htbl
let find t k =
let {outch; htbl = tbl} = t in
- let res = Table.find tbl k in
- res
+ let h = Key.hash k land 0x7FFFFFFF in
+ let lpos = Table.find h tbl in
+ (* First look for already live data *)
+ let find data = match data.obj with
+ | Some (k', v) -> if Key.equal k k' then Some v else None
+ | None -> None
+ in
+ match CList.find_map find lpos with
+ | res -> res
+ | exception Not_found ->
+ (* Otherwise perform I/O and look at the disk cache *)
+ let lpos = List.filter (fun data -> Option.is_empty data.obj) lpos in
+ let () = if CList.is_empty lpos then raise Not_found in
+ let ch = fopen_in t.file in
+ let find data =
+ let () = seek_in ch data.pos in
+ match Marshal.from_channel ch with
+ | (k', v) ->
+ if Key.equal k k' then
+ (* Store the data in memory *)
+ let () = data.obj <- Some (k, v) in
+ Some v
+ else None
+ | exception _ -> None
+ in
+ let lookup () = CList.find_map find lpos in
+ let res = do_under_lock Read (descr_of_out_channel outch) lookup in
+ let () = close_in_noerr ch in
+ res
let memo cache f =
let tbl = lazy (try Some (open_in cache) with _ -> None) in
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 9c75175889..292fbefb84 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -71,7 +71,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
let lookup_map map =
try String.Map.find map !protect_maps
with Not_found ->
- CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
+ CErrors.user_err ~hdr:"lookup_map" (str"Map "++qs map++str"not found")
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
@@ -135,15 +135,11 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
(****************************************************************************)
-let ic c =
- let env = Global.env() in
- let sigma = Evd.from_env env in
+let ic env sigma c =
let c, uctx = Constrintern.interp_constr env sigma c in
(Evd.from_ctx uctx, c)
-let ic_unsafe c = (*FIXME remove *)
- let env = Global.env() in
- let sigma = Evd.from_env env in
+let ic_unsafe env sigma c = (*FIXME remove *)
fst (Constrintern.interp_constr env sigma c)
let decl_constant name univs c =
@@ -170,8 +166,8 @@ let dummy_goal env sigma =
Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in
{Evd.it = gl; Evd.sigma = sigma}
-let constr_of evd v = match Value.to_constr v with
- | Some c -> EConstr.to_constr evd c
+let constr_of sigma v = match Value.to_constr v with
+ | Some c -> EConstr.to_constr sigma c
| None -> failwith "Ring.exec_tactic: anomaly"
let tactic_res = ref [||]
@@ -189,7 +185,7 @@ let get_res =
Tacenv.register_ml_tactic name [| tac |];
entry
-let exec_tactic env evd n f args =
+let exec_tactic env sigma n f args =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
let x = Reference (ArgVar CAst.(make id)) in
@@ -203,11 +199,11 @@ let exec_tactic env evd n f args =
let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in
let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(* Evaluate the whole result *)
- let gl = dummy_goal env evd in
+ let gl = dummy_goal env sigma in
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
- let evd = Evd.minimize_universes gls.Evd.sigma in
- let nf c = constr_of evd c in
- Array.map nf !tactic_res, Evd.universe_context_set evd
+ let sigma = Evd.minimize_universes gls.Evd.sigma in
+ let nf c = constr_of sigma c in
+ Array.map nf !tactic_res, Evd.universe_context_set sigma
let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
let gen_reference n = lazy (Coqlib.lib_ref n)
@@ -222,10 +218,9 @@ let coq_nil = gen_reference "core.list.nil"
let lapp f args = mkApp(Lazy.force f,args)
-let plapp evdref f args =
- let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
- evdref := evd;
- mkApp(fc,args)
+let plapp sigma f args =
+ let sigma, fc = Evarutil.new_global sigma (Lazy.force f) in
+ sigma, mkApp(fc,args)
let dest_rel0 sigma t =
match EConstr.kind sigma t with
@@ -351,14 +346,14 @@ let find_ring_structure env sigma l =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
CErrors.user_err ~hdr:"ring"
- (str"arguments of ring_simplify do not have all the same type")
+ (str"Arguments of ring_simplify do not have all the same type.")
in
List.iter check cl';
(try ring_for_carrier (EConstr.to_constr sigma ty)
with Not_found ->
CErrors.user_err ~hdr:"ring"
- (str"cannot find a declared ring structure over"++
- spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
+ (str"Cannot find a declared ring structure over"++
+ spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"."))
| [] -> assert false
let add_entry e =
@@ -411,16 +406,14 @@ let theory_to_obj : ring_info -> obj =
~cache:cache_th
~subst:(Some subst_th)
-let setoid_of_relation env evd a r =
+let setoid_of_relation env sigma a r =
try
- let evm = !evd in
- let evm, refl = Rewrite.get_reflexive_proof env evm a r in
- let evm, sym = Rewrite.get_symmetric_proof env evm a r in
- let evm, trans = Rewrite.get_transitive_proof env evm a r in
- evd := evm;
- lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
+ let sigma, refl = Rewrite.get_reflexive_proof env sigma a r in
+ let sigma, sym = Rewrite.get_symmetric_proof env sigma a r in
+ let sigma, trans = Rewrite.get_transitive_proof env sigma a r in
+ sigma, lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
with Not_found ->
- error "cannot find setoid relation"
+ CErrors.user_err (str "Cannot find a setoid structure for relation " ++ pr_econstr_env env sigma r ++ str ".")
let op_morph r add mul opp req m1 m2 m3 =
lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
@@ -428,61 +421,59 @@ let op_morph r add mul opp req m1 m2 m3 =
let op_smorph r add mul req m1 m2 =
lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
-let ring_equality env evd (r,add,mul,opp,req) =
- match EConstr.kind !evd req with
- | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
- let setoid = plapp evd coq_eq_setoid [|r|] in
- let op_morph =
+let ring_equality env sigma (r,add,mul,opp,req) =
+ match EConstr.kind sigma req with
+ | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) ->
+ let sigma, setoid = plapp sigma coq_eq_setoid [|r|] in
+ let sigma, op_morph =
match opp with
- Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
- | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
- let sigma = !evd in
+ Some opp -> plapp sigma coq_eq_morph [|r;add;mul;opp|]
+ | None -> plapp sigma coq_eq_smorph [|r;add;mul|] in
let sigma, setoid = Typing.solve_evars env sigma setoid in
let sigma, op_morph = Typing.solve_evars env sigma op_morph in
- evd := sigma;
(setoid,op_morph)
| _ ->
- let setoid = setoid_of_relation (Global.env ()) evd r req in
+ let sigma, setoid = setoid_of_relation env sigma r req in
let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
let add_m, add_m_lem =
try Rewrite.default_morphism signature add
with Not_found ->
- error "ring addition should be declared as a morphism" in
+ CErrors.user_err (str "Ring addition " ++ pr_econstr_env env sigma add ++ str " should be declared as a morphism.") in
let mul_m, mul_m_lem =
try Rewrite.default_morphism signature mul
with Not_found ->
- error "ring multiplication should be declared as a morphism" in
+ CErrors.user_err (str "Ring multiplication " ++ pr_econstr_env env sigma mul ++ str " should be declared as a morphism.") in
let op_morph =
match opp with
| Some opp ->
(let opp_m,opp_m_lem =
try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp
with Not_found ->
- error "ring opposite should be declared as a morphism" in
+ CErrors.user_err (str "Ring opposite " ++ pr_econstr_env env sigma opp ++ str " should be declared as a morphism.") in
let op_morph =
op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
Flags.if_verbose
Feedback.msg_info
- (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
- str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
- str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
- str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
+ (str"Using setoid \""++ pr_econstr_env env sigma req++str"\""++spc()++
+ str"and morphisms \""++pr_econstr_env env sigma add_m ++
+ str"\","++spc()++ str"\""++pr_econstr_env env sigma mul_m++
+ str"\""++spc()++str"and \""++pr_econstr_env env sigma opp_m++
str"\"");
op_morph)
| None ->
(Flags.if_verbose
Feedback.msg_info
- (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
- str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+ (str"Using setoid \""++pr_econstr_env env sigma req ++str"\"" ++ spc() ++
+ str"and morphisms \""++pr_econstr_env env sigma add_m ++
str"\""++spc()++str"and \""++
- pr_econstr_env env !evd mul_m_lem++str"\"");
+ pr_econstr_env env sigma mul_m++str"\"");
op_smorph r add mul req add_m_lem mul_m_lem) in
(setoid,op_morph)
-let build_setoid_params env evd r add mul opp req eqth =
+let build_setoid_params env sigma r add mul opp req eqth =
match eqth with
Some th -> th
- | None -> ring_equality env evd (r,add,mul,opp,req)
+ | None -> ring_equality env sigma (r,add,mul,opp,req)
let dest_ring env sigma th_spec =
let th_typ = Retyping.get_type_of env sigma th_spec in
@@ -515,71 +506,69 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
TacArg(CAst.make (TacCall(CAst.make (t,[]))))
-let make_hyp env evd c =
- let t = Retyping.get_type_of env !evd c in
- plapp evd coq_mkhypo [|t;c|]
+let make_hyp env sigma c =
+ let t = Retyping.get_type_of env sigma c in
+ plapp sigma coq_mkhypo [|t;c|]
-let make_hyp_list env evdref lH =
- let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
- evdref := evd;
- let l =
+let make_hyp_list env sigma lH =
+ let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
+ let sigma, l =
List.fold_right
- (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
- (plapp evdref coq_nil [|carrier|])
+ (fun c (sigma,l) ->
+ let sigma, c = make_hyp env sigma c in
+ plapp sigma coq_cons [|carrier; c; l|]) lH
+ (plapp sigma coq_nil [|carrier|])
in
- let sigma, l' = Typing.solve_evars env !evdref l in
- evdref := sigma;
+ let sigma, l' = Typing.solve_evars env sigma l in
let l' = EConstr.Unsafe.to_constr l' in
- Evarutil.nf_evars_universes !evdref l'
+ sigma, Evarutil.nf_evars_universes sigma l'
-let interp_power env evdref pow =
- let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
- evdref := evd;
+let interp_power env sigma pow =
+ let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
match pow with
| None ->
let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
- (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|])
+ let sigma, c = plapp sigma coq_None [|carrier|] in
+ sigma, (TacArg(CAst.make (TacCall(CAst.make (t,[])))), c)
| Some (tac, spec) ->
let tac =
match tac with
| CstTac t -> Tacintern.glob_tactic t
| Closed lc ->
closed_term_ast (List.map Smartlocate.global_with_alias lc) in
- let spec = make_hyp env evdref (ic_unsafe spec) in
- (tac, plapp evdref coq_Some [|carrier; spec|])
+ let spec = ic_unsafe env sigma spec in
+ let sigma, spec = make_hyp env sigma spec in
+ let sigma, pow = plapp sigma coq_Some [|carrier; spec|] in
+ sigma, (tac, pow)
-let interp_sign env evdref sign =
- let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
- evdref := evd;
+let interp_sign env sigma sign =
+ let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
match sign with
- | None -> plapp evdref coq_None [|carrier|]
+ | None -> plapp sigma coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evdref (ic_unsafe spec) in
- plapp evdref coq_Some [|carrier;spec|]
+ let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
+ plapp sigma coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
-let interp_div env evdref div =
- let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
- evdref := evd;
+let interp_div env sigma div =
+ let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
match div with
- | None -> plapp evdref coq_None [|carrier|]
+ | None -> plapp sigma coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evdref (ic_unsafe spec) in
- plapp evdref coq_Some [|carrier;spec|]
+ let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
+ plapp sigma coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
-let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
+let add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign div =
check_required_library (cdir@["Ring_base"]);
- let env = Global.env() in
let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
- let evd = ref sigma in
- let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
- let (pow_tac, pspec) = interp_power env evd power in
- let sspec = interp_sign env evd sign in
- let dspec = interp_div env evd div in
+ let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
+ let sigma, (pow_tac, pspec) = interp_power env sigma power in
+ let sigma, sspec = interp_sign env sigma sign in
+ let sigma, dspec = interp_div env sigma div in
let rk = reflect_coeff morphth in
let params,ctx =
- exec_tactic env !evd 5 (zltac "ring_lemmas")
+ exec_tactic env sigma 5 (zltac "ring_lemmas")
[sth;ext;rth;pspec;sspec;dspec;rk] in
let lemma1 = params.(3) in
let lemma2 = params.(4) in
@@ -619,16 +608,16 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
ring_post_tac = posttac }) in
()
-let ic_coeff_spec = function
- | Computational t -> Computational (ic_unsafe t)
- | Morphism t -> Morphism (ic_unsafe t)
+let ic_coeff_spec env sigma = function
+ | Computational t -> Computational (ic_unsafe env sigma t)
+ | Morphism t -> Morphism (ic_unsafe env sigma t)
| Abstract -> Abstract
let set_once s r v =
if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
-let process_ring_mods l =
+let process_ring_mods env sigma l =
let kind = ref None in
let set = ref None in
let cst_tac = ref None in
@@ -638,11 +627,11 @@ let process_ring_mods l =
let power = ref None in
let div = ref None in
List.iter(function
- Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
+ Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec env sigma k)
| Const_tac t -> set_once "tactic recognizing constants" cst_tac t
| Pre_tac t -> set_once "preprocess tactic" pre t
| Post_tac t -> set_once "postprocess tactic" post t
- | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+ | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
| Pow_spec(t,spec) -> set_once "power" power (t,spec)
| Sign_spec t -> set_once "sign" sign t
| Div_spec t -> set_once "div" div t) l;
@@ -650,9 +639,11 @@ let process_ring_mods l =
(k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
let add_theory id rth l =
- let (sigma, rth) = ic rth in
- let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
- add_theory0 id (sigma, rth) set k cst (pre,post) power sign div
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma, rth = ic env sigma rth in
+ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods env sigma l in
+ add_theory0 env sigma id rth set k cst (pre,post) power sign div
(*****************************************************************************)
(* The tactics consist then only in a lookup in the ring database and
@@ -663,13 +654,12 @@ let make_args_list sigma rl t =
| [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2]
| _ -> rl
-let make_term_list env evd carrier rl =
- let l = List.fold_right
- (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
- (plapp evd coq_nil [|carrier|])
+let make_term_list env sigma carrier rl =
+ let sigma, l = List.fold_right
+ (fun x (sigma,l) -> plapp sigma coq_cons [|carrier;x;l|]) rl
+ (plapp sigma coq_nil [|carrier|])
in
- let sigma, l = Typing.solve_evars env !evd l in
- evd := sigma; l
+ Typing.solve_evars env sigma l
let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
let tacarg expr =
@@ -695,12 +685,13 @@ let ring_lookup (f : Value.t) lH rl t =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let rl = make_args_list sigma rl t in
- let evdref = ref sigma in
let e = find_ring_structure env sigma rl in
- let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
- let lH = carg (make_hyp_list env evdref lH) in
+ let sigma, l = make_term_list env sigma (EConstr.of_constr e.ring_carrier) rl in
+ let rl = Value.of_constr l in
+ let sigma, l = make_hyp_list env sigma lH in
+ let lH = carg l in
let ring = ltac_ring_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (ring@[lH;rl]))
end
(***********************************************************************)
@@ -758,23 +749,23 @@ let sfield_theory = my_reference "semi_field_theory"
let af_ar = my_reference"AF_AR"
let f_r = my_reference"F_R"
let sf_sr = my_reference"SF_SR"
-let dest_field env evd th_spec =
- let th_typ = Retyping.get_type_of env !evd th_spec in
- match EConstr.kind !evd th_typ with
+let dest_field env sigma th_spec =
+ let th_typ = Retyping.get_type_of env sigma th_spec in
+ match EConstr.kind sigma th_typ with
| App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
- when isRefX !evd (Lazy.force afield_theory) f ->
- let rth = plapp evd af_ar
+ when isRefX sigma (Lazy.force afield_theory) f ->
+ let sigma, rth = plapp sigma af_ar
[|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
(None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
| App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
- when isRefX !evd (Lazy.force field_theory) f ->
- let rth =
- plapp evd f_r
+ when isRefX sigma (Lazy.force field_theory) f ->
+ let sigma, rth =
+ plapp sigma f_r
[|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
(Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
| App(f,[|r;zero;one;add;mul;div;inv;req|])
- when isRefX !evd (Lazy.force sfield_theory) f ->
- let rth = plapp evd sf_sr
+ when isRefX sigma (Lazy.force sfield_theory) f ->
+ let sigma, rth = plapp sigma sf_sr
[|r;zero;one;add;mul;div;inv;req;th_spec|] in
(Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
| _ -> error "bad field structure"
@@ -804,14 +795,14 @@ let find_field_structure env sigma l =
let ty' = Retyping.get_type_of env sigma c in
if not (Reductionops.is_conv env sigma ty ty') then
CErrors.user_err ~hdr:"field"
- (str"arguments of field_simplify do not have all the same type")
+ (str"Arguments of field_simplify do not have all the same type.")
in
List.iter check cl';
(try field_for_carrier (EConstr.to_constr sigma ty)
with Not_found ->
CErrors.user_err ~hdr:"field"
- (str"cannot find a declared field structure over"++
- spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
+ (str"Cannot find a declared field structure over"++
+ spc()++str"\""++pr_econstr_env env sigma ty++str"\"."))
| [] -> assert false
let add_field_entry e =
@@ -860,14 +851,14 @@ let ftheory_to_obj : field_info -> obj =
~cache:cache_th
~subst:(Some subst_th)
-let field_equality evd r inv req =
- match EConstr.kind !evd req with
- | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
+let field_equality env sigma r inv req =
+ match EConstr.kind sigma req with
+ | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) ->
let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
let c = EConstr.of_constr c in
mkApp(c,[|r;r;inv|])
| _ ->
- let _setoid = setoid_of_relation (Global.env ()) evd r req in
+ let _setoid = setoid_of_relation env sigma r req in
let signature = [Some (r,Some req)],Some(r,Some req) in
let inv_m, inv_m_lem =
try Rewrite.default_morphism signature inv
@@ -875,24 +866,22 @@ let field_equality evd r inv req =
error "field inverse should be declared as a morphism" in
inv_m_lem
-let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory0 env sigma name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
let open Constr in
check_required_library (cdir@["Field_tac"]);
- let (sigma,fth) = ic fth in
- let env = Global.env() in
- let evd = ref sigma in
+ let (sigma,fth) = ic env sigma fth in
let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
- dest_field env evd fth in
- let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+ dest_field env sigma fth in
+ let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
let eqth = Some(sth,ext) in
- let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
- let (pow_tac, pspec) = interp_power env evd power in
- let sspec = interp_sign env evd sign in
- let dspec = interp_div env evd odiv in
- let inv_m = field_equality evd r inv req in
+ let _ = add_theory0 env sigma name rth eqth morphth cst_tac (None,None) power sign odiv in
+ let sigma, (pow_tac, pspec) = interp_power env sigma power in
+ let sigma, sspec = interp_sign env sigma sign in
+ let sigma, dspec = interp_div env sigma odiv in
+ let inv_m = field_equality env sigma r inv req in
let rk = reflect_coeff morphth in
let params,ctx =
- exec_tactic env !evd 9 (field_ltac"field_lemmas")
+ exec_tactic env sigma 9 (field_ltac"field_lemmas")
[sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in
let lemma1 = params.(3) in
let lemma2 = params.(4) in
@@ -940,7 +929,7 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
field_pre_tac = pretac;
field_post_tac = posttac }) in ()
-let process_field_mods l =
+let process_field_mods env sigma l =
let kind = ref None in
let set = ref None in
let cst_tac = ref None in
@@ -951,22 +940,24 @@ let process_field_mods l =
let power = ref None in
let div = ref None in
List.iter(function
- Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
+ Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec env sigma k)
| Ring_mod(Const_tac t) ->
set_once "tactic recognizing constants" cst_tac t
| Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
| Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
- | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+ | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
| Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
| Ring_mod(Sign_spec t) -> set_once "sign" sign t
| Ring_mod(Div_spec t) -> set_once "div" div t
- | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
+ | Inject i -> set_once "infinite property" inj (ic_unsafe env sigma i)) l;
let k = match !kind with Some k -> k | None -> Abstract in
- (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
+ (env, sigma, k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
let add_field_theory id t mods =
- let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in
- add_field_theory0 id t set k cst_tac inj (pre,post) power sign div
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let (env,sigma,k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods env sigma mods in
+ add_field_theory0 env sigma id t set k cst_tac inj (pre,post) power sign div
let ltac_field_structure e =
let req = carg e.field_req in
@@ -987,10 +978,11 @@ let field_lookup (f : Value.t) lH rl t =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let rl = make_args_list sigma rl t in
- let evdref = ref sigma in
let e = find_field_structure env sigma rl in
- let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
- let lH = carg (make_hyp_list env evdref lH) in
+ let sigma, c = make_term_list env sigma (EConstr.of_constr e.field_carrier) rl in
+ let rl = Value.of_constr c in
+ let sigma, l = make_hyp_list env sigma lH in
+ let lH = carg l in
let field = ltac_field_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (field@[lH;rl]))
end
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index ccdf5fa68e..f06b460ee9 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1792,7 +1792,7 @@ GRAMMAR EXTEND Gram
{ ssrdotac_expr ~loc noindex m tac clauses }
| IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
{ ssrdotac_expr ~loc noindex Once tac clauses }
- | IDENT "do"; n = int_or_var; m = ssrmmod;
+ | IDENT "do"; n = nat_or_var; m = ssrmmod;
tac = ssrdotac; clauses = ssrclauses ->
{ ssrdotac_expr ~loc (mk_index ~loc n) m tac clauses }
] ];
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bd514f15d5..a4aa08300d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u =
let nb_cs_proj_args pc f u =
let na k =
- List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in
+ List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
let nargs_of_proj t = match kind t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 54fdea0860..74535a10d3 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -141,7 +141,7 @@ let interp_search_notation ?loc tag okey =
let rec sub () = function
| NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
| c ->
- glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
+ glob_constr_of_notation_constr_with_binders ?loc (fun _ x t -> (), None, x, Explicit, t) sub () c in
let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:41:35 +0000