diff options
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index de63c557d..d58b6ad13 100644 --- a/dev/base_include +++ b/dev/base_include @@ -86,6 +86,7 @@ open Cbv open Classops open Clenv open Clenvtac +open Constr_matching open Glob_term open Glob_ops open Coercion diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 161cffa86..e28180713 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, c1) :: subargs env lc in + let sub = (env, hd) :: (env, c1) :: subargs env lc in let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> |