From b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Jun 2016 15:12:05 +0200 Subject: A slight phase of documentation and uniformization of names of functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do. --- interp/constrintern.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4a451634d..50252a368 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -526,7 +526,7 @@ let rec subst_iterator y t = function | GVar (_,id) as x -> if Id.equal id y then t else x | x -> map_glob_constr (subst_iterator y t) x -let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = +let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) @@ -649,7 +649,7 @@ let intern_notation intern env lvar loc ntn fullargs = let terms = make_subst ids args in let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in - subst_aconstr_in_glob_constr loc intern lvar + instantiate_notation_constr loc intern lvar (terms, termlists, binders) (Id.Map.empty, env) c (**********************************************************************) @@ -759,7 +759,7 @@ let intern_qualid loc qid intern env lvar us args = let subst = (terms, Id.Map.empty, Id.Map.empty) in let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in - let c = subst_aconstr_in_glob_constr loc intern lvar subst infos c in + let c = instantiate_notation_constr loc intern lvar subst infos c in let c = match us, c with | None, _ -> c | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) -- cgit v1.2.3