diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/README | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 10 |
5 files changed, 7 insertions, 15 deletions
diff --git a/plugins/cc/README b/plugins/cc/README index c616b5daab..7df7b971e8 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -9,7 +9,7 @@ Files : - ccalgo.ml : congruence closure algorithm - ccproof.ml : proof generation code -- cctac.ml4 : the tactic itself +- cctac.mlg : the tactic itself - CCSolve.v : a small Ltac tactic based on congruence Known Bugs : the congruence tactic can fail due to type dependencies. diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index ef012e5092..f47a14cdc7 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file uses the (non-compressed) union-find structure to generate *) -(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +(* proof-trees that will be transformed into proof-terms in cctac.mlg *) open CErrors open Constr diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 96a3d00dc2..be9259861a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -380,7 +380,7 @@ let check_inside_module () = warn_extraction_inside_module () let check_inside_section () = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 9b52b710c1..1b00a93834 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -182,10 +182,6 @@ let mkCLambdaN_simple bl c = match bl with let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc -let map_int_or_var f = function - | ArgArg x -> ArgArg (f x) - | ArgVar _ as y -> y - let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } let merge_occurrences loc cl = function @@ -269,7 +265,7 @@ GRAMMAR EXTEND Gram [ [ 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 (map_int_or_var abs) (n::nl)) } ] ] + { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ] ; occs: [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index b6e7dd64b0..bf5d49f678 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -76,25 +76,21 @@ let subst_and_short_name f (c,n) = (* assert (n=None); *)(* since tacdef are strictly globalized *) (f c,None) -let subst_or_var f = let open Locus in function - | ArgVar _ as x -> x - | ArgArg x -> ArgArg (f x) - let subst_located f = Loc.map f let subst_reference subst = - subst_or_var (subst_located (subst_kn subst)) + Locusops.or_var_map (subst_located (subst_kn subst)) (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as Print. It is also used for non-evaluable references. *) let subst_global_reference subst = - subst_or_var (subst_located (subst_global_reference subst)) + Locusops.or_var_map (subst_located (subst_global_reference subst)) let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in - subst_or_var (subst_and_short_name subst_eval_ref) + Locusops.or_var_map (subst_and_short_name subst_eval_ref) let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) |