diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 14:03:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:32 +0200 |
| commit | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (patch) | |
| tree | 32282ac2f1198738c8c545b19215ff0a0d9ef6ce /pretyping/typeclasses.ml | |
| parent | b720cd3cbefa46da784b68a8e016a853f577800c (diff) | |
Referring to evars by names. Added a parser for evars (but parsing of
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a3bd06ed5..c74ed19a8 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -497,7 +497,7 @@ let is_instance = function | _ -> false let is_implicit_arg = function -| Evar_kinds.GoalEvar -> false +| Evar_kinds.GoalEvar _ -> false | _ -> true (* match k with *) (* ImplicitArg (ref, (n, id), b) -> true *) @@ -538,10 +538,10 @@ open Evar_kinds type evar_filter = existential_key -> Evar_kinds.t -> bool let all_evars _ _ = true -let all_goals _ = function GoalEvar -> true | _ -> false +let all_goals _ = function GoalEvar _ -> true | _ -> false let no_goals ev evi = not (all_goals ev evi) let no_goals_or_obligations _ = function - | GoalEvar | QuestionMark _ -> false + | GoalEvar _ | QuestionMark _ -> false | _ -> true let mark_resolvability filter b sigma = |