aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r--plugins/ltac/rewrite.ml57
1 files changed, 29 insertions, 28 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index acd7a30c43..d32a2faefc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
@@ -1568,7 +1570,8 @@ 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
- match clause, prf with
+ let gls = List.map Proofview.with_empty_state gls in
+ match clause, prf with
| Some id, Some p ->
let tac = tclTHENLIST [
Refine.refine ~typecheck:true (fun h -> (h,p));
@@ -1770,12 +1773,11 @@ let rec strategy_of_ast = function
(* By default the strategy for "rewrite_db" is top-down *)
-let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l)
let declare_an_instance n s args =
- (((Loc.tag @@ Name n),None), Explicit,
- CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None),
- args))
+ (((CAst.make @@ Name n),None), Explicit,
+ CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args))
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
@@ -1789,17 +1791,17 @@ let anew_instance global binders instance fields =
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)]
let declare_instance_sym global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)]
let declare_instance_trans global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
in anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
+ [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)]
let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
@@ -1823,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1);
- (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+ (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)])
| (None, Some lemma2, Some lemma3) ->
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2);
- (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2);
+ (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)])
| (Some lemma1, Some lemma2, Some lemma3) ->
let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1840,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)])
+ [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
@@ -1896,7 +1898,6 @@ let declare_projection n instance_id r =
let build_morphism_signature env sigma m =
let m,ctx = Constrintern.interp_constr env sigma m in
- let m = EConstr.of_constr m in
let sigma = Evd.from_ctx ctx in
let t = Typing.unsafe_type_of env sigma m in
let cstrs =
@@ -1920,7 +1921,7 @@ let build_morphism_signature env sigma m =
in
let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
let evd = solve_constraints env !evd in
- let evd = Evd.nf_constraints evd in
+ let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
Evd.evar_universe_context evd, m
@@ -1949,16 +1950,16 @@ let add_setoid global binders a aeq t n =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
- (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+ [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+ (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
let make_tactic name =
let open Tacexpr in
let tacpath = Libnames.qualid_of_string name in
- let tacname = Qualid (Loc.tag tacpath) in
- TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
+ let tacname = CAst.make @@ Qualid tacpath in
+ TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, []))))
let warn_add_morphism_deprecated =
CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
@@ -2006,9 +2007,9 @@ let add_morphism glob binders m s n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance =
- (((Loc.tag @@ Name instance_id),None), Explicit,
+ (((CAst.make @@ Name instance_id),None), Explicit,
CAst.make @@ CAppExpl (
- (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+ (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 02:41:01 +0000