diff options
| author | Arnaud Spiwack | 2013-12-06 16:45:10 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-06 16:45:10 +0100 |
| commit | 84c4f0e509dc6cde3a53dda3ba946077cc23ad95 (patch) | |
| tree | 814fe7e08bac33e433c001d51a57c2a3d0cd2fc0 | |
| parent | 2bbe6a88b840a4857f683fd6ee8cfc37ad7770c7 (diff) | |
Fix test-suite/success/evars.v.
In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected).
| -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 a5e822862e..b0a4ebea41 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1681,7 +1681,7 @@ let build_inversion_problem loc env sigma tms t = let sub_tms = List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) -> let na = if List.is_empty deps then Anonymous else force_name na in - Pushed (false,((tm,tmtyp),deps,na))) + Pushed (true,((tm,tmtyp),deps,na))) dep_sign decls in let subst = List.map (fun (na,t) -> (na,lift n t)) subst in (* [eqn1] is the first clause of the auxiliary pattern-matching that |