diff options
| author | Maxime Dénès | 2019-04-05 12:18:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:45 +0200 |
| commit | 5af486406e366bf23558311a7367e573c617e078 (patch) | |
| tree | e2996582ca8eab104141dd75b82ac1777e53cb72 /interp/notation_ops.ml | |
| parent | f6dc8b19760aaf0cc14e6d9eb2d581ba1a05a762 (diff) | |
Remove calls to global env in Inductiveops
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1f1cf4506f..9801e56ca1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function | GApp (t, l) -> begin match DAst.get t with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) | _ -> raise No_match @@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let env = Global.env () in + let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in |