aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/indfun.ml78
-rw-r--r--plugins/ltac/coretactics.ml48
-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_rewrite.ml42
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/tauto.ml3
-rw-r--r--plugins/ltac/tauto_plugin.mlpack1
10 files changed, 48 insertions, 53 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ad04e430c..35f092958 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -576,50 +576,44 @@ let map_option f = function
| Some v -> Some (f v)
open Constrexpr
-open Topconstr
-let make_assoc assoc l1 l2 =
- let fold assoc a b = match a, b with
- | (_, Name na), (_, Name id) -> Id.Map.add na id assoc
- | _, _ -> assoc
- in
- List.fold_left2 fold assoc l1 l2
-
-let rec rebuild_bl (aux,assoc) bl typ =
- match bl,typ with
- | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
- | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
- rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
- | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } ->
- rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
+let rec rebuild_bl aux bl typ =
+ match bl,typ with
+ | [], _ -> List.rev aux,typ
+ | (CLocalAssum(nal,bk,_))::bl',typ ->
+ rebuild_nal aux bk bl' nal typ
+ | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } ->
+ rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux)
bl' typ'
| _ -> assert false
- and rebuild_nal (aux,assoc) bk bl' nal lnal typ =
- match nal, typ.CAst.v with
- | [], _ -> rebuild_bl (aux,assoc) bl' typ
- | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
- | _,CProdN((nal',bk',nal't)::rest,typ') ->
- let lnal' = List.length nal' in
- if lnal' >= lnal
- then
- let old_nal',new_nal' = List.chop lnal nal' in
- let nassoc = make_assoc assoc old_nal' nal in
- let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
- rebuild_bl ((assum :: aux), nassoc) bl'
- (if List.is_empty new_nal' && List.is_empty rest
- then typ'
- else CAst.make @@ if List.is_empty new_nal'
- then CProdN(rest,typ')
- else CProdN(((new_nal',bk',nal't)::rest),typ'))
- else
- let captured_nal,non_captured_nal = List.chop lnal' nal in
- let nassoc = make_assoc assoc nal' captured_nal in
- let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
- rebuild_nal ((assum :: aux), nassoc)
- bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ'))
- | _ -> assert false
-
-let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
+and rebuild_nal aux bk bl' nal typ =
+ match nal,typ with
+ | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
+ | [], _ -> rebuild_bl aux bl' typ
+ | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
+ if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+ then
+ let assum = CLocalAssum([na],bk',nal't) in
+ let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ rebuild_nal
+ (assum::aux)
+ bk
+ bl'
+ nal
+ (CAst.make @@ CProdN(new_rest,typ'))
+ else
+ let assum = CLocalAssum([na'],bk',nal't) in
+ let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ rebuild_nal
+ (assum::aux)
+ bk
+ bl'
+ (na::nal)
+ (CAst.make @@ CProdN(new_rest,typ'))
+ | _ ->
+ assert false
+
+let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
@@ -629,7 +623,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
- let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in
+ let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in
(((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixpoint_exprl constr_expr_typel
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb..50013f558 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -17,7 +17,7 @@ open Stdarg
open Extraargs
open Names
-DECLARE PLUGIN "coretactics"
+DECLARE PLUGIN "ltac_plugin"
(** Basic tactics *)
@@ -324,11 +324,11 @@ let initial_atomic () =
"fresh", TacArg(Loc.tag @@ TacFreshId [])
]
-let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
(* First-class Ltac access to primitive blocks *)
-let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
let register_list_tactical name f =
@@ -356,4 +356,4 @@ let initial_tacticals () =
"solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
]
-let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
+let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7259faecd..36df25cc7 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -28,7 +28,7 @@ open Equality
open Misctypes
open Proofview.Notations
-DECLARE PLUGIN "extratactics"
+DECLARE PLUGIN "ltac_plugin"
(**********************************************************************)
(* replace, discriminate, injection, simplify_eq *)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfd8e88a9..6145e373b 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -18,7 +18,7 @@ open Pcoq.Constr
open Pltac
open Hints
-DECLARE PLUGIN "g_auto"
+DECLARE PLUGIN "ltac_plugin"
(* Hint bases *)
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 905cfd02a..63451210c 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,7 +13,7 @@ open Class_tactics
open Stdarg
open Tacarg
-DECLARE PLUGIN "g_class"
+DECLARE PLUGIN "ltac_plugin"
(** Options: depth, debug and transparency settings. *)
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 570cd4e69..dceefeaa1 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -17,7 +17,7 @@
open API
open Eqdecide
-DECLARE PLUGIN "g_eqdecide"
+DECLARE PLUGIN "ltac_plugin"
TACTIC EXTEND decide_equality
| [ "decide" "equality" ] -> [ decideEqualityGoal ]
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index e6ddc5cc1..3e6f42006 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -27,7 +27,7 @@ open Pcoq.Prim
open Pcoq.Constr
open Pltac
-DECLARE PLUGIN "g_rewrite"
+DECLARE PLUGIN "ltac_plugin"
type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index af1c7149d..12b4c81fc 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -21,7 +21,6 @@ G_auto
G_class
Rewrite
G_rewrite
-Tauto
G_eqdecide
G_tactic
G_ltac
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 2a8ed7238..71f7082e7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,13 +13,14 @@ open Hipattern
open Names
open Geninterp
open Misctypes
+open Ltac_plugin
open Tacexpr
open Tacinterp
open Util
open Tacticals.New
open Proofview.Notations
-let tauto_plugin = "tauto"
+let tauto_plugin = "tauto_plugin"
let () = Mltop.add_known_module tauto_plugin
let assoc_var s ist =
diff --git a/plugins/ltac/tauto_plugin.mlpack b/plugins/ltac/tauto_plugin.mlpack
new file mode 100644
index 000000000..b3618018e
--- /dev/null
+++ b/plugins/ltac/tauto_plugin.mlpack
@@ -0,0 +1 @@
+Tauto
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 19:24:05 +0000