diff options
author | 2015-09-09 11:00:35 +0200 | |
---|---|---|
committer | 2015-09-09 11:08:53 +0200 | |
commit | 952cd3e53d630120dc1319c93421fe2708252b54 (patch) | |
tree | 05326c26788c6edaac980c69a0187e3875bb8de1 /pretyping | |
parent | 9510a3994210f545119ea35cdad43facededb6a2 (diff) | |
parent | 703e5b595a4a96dc9ff3df7ad10f90a238a061b6 (diff) |
Merge remote-tracking branch 'origin/v8.5' into trunk
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ef196e0a7..05e09b968 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1466,6 +1466,14 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = compile pb in let sigma = !(pb.evdref) in + (* If the "match" was orginally over a variable, as in "match x with + O => true | n => n end", we give preference to non-expansion in + the default clause (i.e. "match x with O => true | n => n end" + rather than "match x with O => true | S p => S p end"; + computationally, this avoids reallocating constructors in cbv + evaluation; the drawback is that it might duplicate the instances + of the term to match when the corresponding variable is + substituted by a non-evaluated expression *) if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then (* Try to compile first using non expanded alias *) try @@ -1473,6 +1481,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) + (* Could be needed in case of dependent return clause *) pb.evdref := sigma; f expanded expanded_typ else @@ -1480,6 +1489,8 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = try f expanded expanded_typ with e when precatchable_exception e -> (* Try then to compile using non expanded alias *) + (* Could be needed in case of a recursive call which requires to + be on a variable for size reasons *) pb.evdref := sigma; if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) else just_pop () |