diff options
| -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 |