aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml42
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/g_eqdecide.ml42
-rw-r--r--plugins/ltac/g_ltac.ml44
-rw-r--r--plugins/ltac/g_obligations.ml44
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/profile_ltac_tactics.ml42
-rw-r--r--plugins/ltac/rewrite.ml13
11 files changed, 8 insertions, 29 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 2769802cf..7d2c4d082 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Util
open Locus
open Misctypes
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index bb01aca55..4c6d3c2d3 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e3965b94..286f9d95d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 90a44708f..f74d24db0 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ed2d9da63..014433ac4 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Class_tactics
open Stdarg
open Tacarg
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 549436902..f705778fc 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -12,8 +12,6 @@
(* by Eduardo Gimenez *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Eqdecide
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index cc7ce339b..9ef819569 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
DECLARE PLUGIN "ltac_plugin"
open Util
@@ -17,7 +15,7 @@ open Tacexpr
open Misctypes
open Genarg
open Genredexpr
-open Tok (* necessary for camlp4 *)
+open Tok (* necessary for camlp5 *)
open Names
open Pcoq
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index f6cc3833a..e251b1049 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -6,11 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
(*
Syntax for the subtac terms and types.
- Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
+ Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
open Libnames
open Constrexpr
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index ea1808a25..2459a09bc 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
(* Syntax for rewriting with strategies *)
open Names
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 9864ffeb6..7a75662be 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
(** Ltac profiling entrypoints *)
open Profile_ltac
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3cbb11001..acd7a30c4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -210,9 +210,9 @@ end) = struct
let t = Reductionops.whd_all env (goalevars evars) ty in
match EConstr.kind (goalevars evars) t, l with
| Prod (na, ty, b), obj :: cstrs ->
- let b = Reductionops.nf_betaiota (goalevars evars) b in
+ let b = Reductionops.nf_betaiota env (goalevars evars) b in
if noccurn (goalevars evars) 1 b (* non-dependent product *) then
- let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+ let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
let evars, relty = mk_relty evars env ty obj in
let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
@@ -221,7 +221,7 @@ end) = struct
let (evars, b, arg, cstrs) =
aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
in
- let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+ let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
@@ -231,7 +231,7 @@ end) = struct
| _, [] ->
(match finalcstr with
| None | Some (_, None) ->
- let t = Reductionops.nf_betaiota (fst evars) ty in
+ let t = Reductionops.nf_betaiota env (fst evars) ty in
let evars, rel = mk_relty evars env t None in
evars, t, rel, [t, Some rel]
| Some (t, Some rel) -> evars, t, rel, [t, Some rel])
@@ -1557,9 +1557,8 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
(** For compatibility *)
- let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
- let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
- let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
+ let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+ let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-02 11:03:51 +0000