diff options
| author | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
| commit | b3a8761790c0905aad8e5d3102fab606fe5e7fd6 (patch) | |
| tree | ce5fbe8cb717bad677ad755e7875413d3e5d0e84 /interp/declare.ml | |
| parent | 9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (diff) | |
| parent | 886a9c2fb25e32bd87b3fce38023b3e701134d23 (diff) | |
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index dfa84f278e..f6d7b45c3c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -135,7 +135,7 @@ let set_declare_scheme f = declare_scheme := f let update_tables c = declare_constant_implicits c; Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c) + Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) let register_side_effect (c, role) = let o = inConstant { @@ -275,7 +275,7 @@ let inVariable : variable_obj -> obj = let declare_variable id obj = let oname = add_leaf id (inVariable (Inr (id,obj))) in declare_var_implicits id; - Notation.declare_ref_arguments_scope (VarRef id); + Notation.declare_ref_arguments_scope Evd.empty (VarRef id); Heads.declare_head (EvalVarRef id); oname @@ -283,9 +283,9 @@ let declare_variable id obj = let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope (IndRef (kn,i)); + Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); for j=1 to List.length lc do - Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); done) mie.mind_entry_inds let inductive_names sp kn mie = |