diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 11:36:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:57 +0100 |
| commit | c1cab3ba606f7034f2785f06c0d3892bca3976cf (patch) | |
| tree | 19918420f7e4b64be31953dae8f51c981e638f4a /pretyping | |
| parent | 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (diff) | |
Removing cumbersome location in multiple patterns.
This is to have a better symmetry between CCases and GCases.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4f3669a2b..1207c967b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1566,11 +1566,9 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,lpat,rhs)) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = |