diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 2 |
6 files changed, 14 insertions, 14 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5163ec7b3..007d139a3 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac -(** Open term to lambda-term coercion {{{ ************************************) +(** Open term to lambda-term coercion *)(* {{{ ************************************) (* This operation takes a goal gl and an open term (sigma, t), and *) (* returns a term t' where all the new evars in sigma are abstracted *) @@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; @@ -1128,7 +1128,7 @@ let interp_clr sigma = function (** Basic tacticals *) -(** Multipliers {{{ ***********************************************************) +(** Multipliers *)(* {{{ ***********************************************************) (* tactical *) @@ -1168,7 +1168,7 @@ let tclMULT = function let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr)) let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) -(** }}} *) +(* }}} *) (** Generalize tactic *) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 70f73c1fe..2bed8b624 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr let old_tac = V82.tactic -(** Name generation {{{ *******************************************************) +(** Name generation *)(* {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag) (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. {{{ **************************************************) +(** Tactical extensions. *)(* {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 21ad6e6ce..cdf1c6f95 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) let hidden_goal_tag = "the_hidden_goal" diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index f37452613..e3941c1c5 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -127,7 +127,7 @@ GEXTEND Gram END (* }}} *) -(** Vernacular commands: Prenex Implicits and Search {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -461,7 +461,7 @@ END (* }}} *) -(** View hint database and View application. {{{ ******************************) +(** View hint database and View application. *)(* {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 1f1a63dac..62c35d6df 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -70,7 +70,7 @@ let _ = Goptions.optwrite = debug } let pp s = !pp_ref s -(** Utils {{{ *****************************************************************) +(** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind c with App (f, a) -> f, a | _ -> c, [| |] @@ -179,7 +179,7 @@ let nf_evar sigma c = (* }}} *) -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index cd5676f28..07d0f9757 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -74,7 +74,7 @@ val interp_cpattern : pattern (** The set of occurrences to be matched. The boolean is set to true - * to signal the complement of this set (i.e. {-1 3}) *) + * to signal the complement of this set (i.e. \{-1 3\}) *) type occ = (bool * int list) option (** [subst e p t i]. [i] is the number of binders |