- let l1 =
- CicNotationParser.refresh_uri_in_checked_l1_pattern
- ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
- let l2 = NotationUtil.refresh_uri_in_term
- ~refresh_uri_in_term ~refresh_uri_in_reference l2
- in
- basic_eval_output_notation (l1,l2)
+ if not alias_only then
+ let l1 =
+ CicNotationParser.refresh_uri_in_checked_l1_pattern
+ ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+ let l2 = NotationUtil.refresh_uri_in_term
+ ~refresh_uri_in_term ~refresh_uri_in_reference l2
+ in
+ basic_eval_output_notation (l1,l2) status
+ else
+ status