diff options
| author | Hugo Herbelin | 2015-01-08 18:18:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-08 19:05:14 +0100 |
| commit | d08532d5344d96d10604760fa44109c9d56e73ce (patch) | |
| tree | 2f5b472f526a6ad9f72cb57bde4503501f9c7129 /pretyping | |
| parent | b584c5529f7195849b0dd4f1eebf7c73c46f60db (diff) | |
Avoiding introducing yet another convention in naming files.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml (renamed from pretyping/constrMatching.ml) | 0 | ||||
| -rw-r--r-- | pretyping/constr_matching.mli (renamed from pretyping/constrMatching.mli) | 0 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 10 |
4 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constr_matching.ml index ad4c678cbd..ad4c678cbd 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constr_matching.ml diff --git a/pretyping/constrMatching.mli b/pretyping/constr_matching.mli index a4e797dae0..a4e797dae0 100644 --- a/pretyping/constrMatching.mli +++ b/pretyping/constr_matching.mli diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index b189360c07..25d17c7c9f 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,7 +20,7 @@ Miscops Glob_ops Redops Patternops -ConstrMatching +Constr_matching Tacred Typeclasses_errors Typeclasses diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2064fb6e17..9a778e0181 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -943,9 +943,9 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head env sigma c t = match kind_of_term t with - | App (f,_) -> ConstrMatching.matches env sigma c f - | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p)) - | _ -> raise ConstrMatching.PatternMatchingFailure + | App (f,_) -> Constr_matching.matches env sigma c f + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) + | _ -> raise Constr_matching.PatternMatchingFailure let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false @@ -980,7 +980,7 @@ let e_contextually byhead (occs,c) f env sigma t = try let subst = if byhead then matches_head env sigma c t - else ConstrMatching.matches env sigma c t in + else Constr_matching.matches env sigma c t in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in @@ -996,7 +996,7 @@ let e_contextually byhead (occs,c) f env sigma t = end else traverse_below nested envc t - with ConstrMatching.PatternMatchingFailure -> + with Constr_matching.PatternMatchingFailure -> traverse_below nested envc t and traverse_below nested envc t = (* when byhead, find other occurrences without matching again partial |