diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /plugins/ssr | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
4 files changed, 7 insertions, 6 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index bb8a0faf2e..11e282e4f5 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -104,6 +104,7 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats type ssrfwdid = Id.t + (** Binders (for fwd tactics) *) type 'term ssrbind = | Bvar of Name.t diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index efc4a2c743..cd9af84ed9 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -263,7 +263,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 0553260472..18b4aeab1e 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -86,9 +86,9 @@ end (* }}} *************************************************************** *) open State -(** [=> *] ****************************************************************) -(** [nb_assums] returns the number of dependent premises *) -(** Warning: unlike [nb_deps_assums], it does not perform reduction *) +(***[=> *] ****************************************************************) +(** [nb_assums] returns the number of dependent premises + Warning: unlike [nb_deps_assums], it does not perform reduction *) let rec nb_assums cur env sigma t = match EConstr.kind sigma t with | Prod(name,ty,body) -> @@ -148,7 +148,7 @@ let tac_case t = Ssrelim.ssrscasetac t end -(** [=> [: id]] ************************************************************) +(***[=> [: id]] ************************************************************) [@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4ed75cdbe4..191a4e9a20 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in + let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else |