diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 33b1e8136..5c3e8fe92 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -183,7 +183,7 @@ let complete_history = glob_pattern_of_partial_history [] (* This is to build glued pattern-matching history and alias bodies *) -let rec pop_history_pattern = function +let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> |