diff options
| author | Guillaume Melquiond | 2016-01-02 16:50:02 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-02 16:50:02 +0100 |
| commit | 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e (patch) | |
| tree | d36a8ce954b3fb4d3ba0f0b93ca80816620654fc | |
| parent | a5e1b40b93e47a278746ee6752474891cd856c29 (diff) | |
Remove useless rec flags.
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | ide/sentence.ml | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index d91b90caa2..8476db6646 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1230,7 +1230,7 @@ let pr_decl ((id,b,_),ok) = | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") -let rec pr_evar_source = function +let pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> diff --git a/ide/sentence.ml b/ide/sentence.ml index dd6b10a461..8195051c6c 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -63,13 +63,13 @@ let grab_sentence_start (iter:GText.iter) soi = (** Search forward the first character immediately after a sentence end *) -let rec grab_sentence_stop (start:GText.iter) = +let grab_sentence_stop (start:GText.iter) = (forward_search is_sentence_end start)#forward_char (** Search forward the first character immediately after a "." sentence end (and not just a "\{" or "\}" or comment end *) -let rec grab_ending_dot (start:GText.iter) = +let grab_ending_dot (start:GText.iter) = let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in (forward_search is_ending_dot start)#forward_char diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 50a543968a..7800f1edb3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1268,7 +1268,7 @@ module Make let pr_pat_and_constr_expr pr ((c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6d20bc3cdb..1349d55177 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2130,7 +2130,7 @@ let rewrite_hyp assert_style l2r id = Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])) end } -let rec prepare_naming loc = function +let prepare_naming loc = function | IntroIdentifier id -> NamingMustBe (loc,id) | IntroAnonymous -> NamingAvoid [] | IntroFresh id -> NamingBasedOn (id,[]) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3308903dd7..3ac537297e 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -260,7 +260,7 @@ let explain_generalization env sigma (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let rec explain_unification_error env sigma p1 p2 = function +let explain_unification_error env sigma p1 p2 = function | None -> mt() | Some e -> let rec aux p1 p2 = function |