diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:12:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:25:14 +0200 |
| commit | b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d (patch) | |
| tree | 2a90fbdf676aea46265fc5dd45ed220a47d9ff82 /plugins/funind/glob_term_to_relation.ml | |
| parent | 4648732544f43ad87266f33967995b29d2b8338b (diff) | |
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.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 72205e2bb..c424fe122 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1217,7 +1217,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) if Array.for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined') + Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') rels_params then l := param::!l |