aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:50:02 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:50:02 +0100
commit2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e (patch)
treed36a8ce954b3fb4d3ba0f0b93ca80816620654fc /engine/evd.ml
parenta5e1b40b93e47a278746ee6752474891cd856c29 (diff)
Remove useless rec flags.
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index d91b90caa..8476db664 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 ->