let inject_unification_hint =
let basic_eval_unification_hint (t,n)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
let inject_unification_hint =
let basic_eval_unification_hint (t,n)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
-let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
let inject_interpretation =
let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
let inject_interpretation =
let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
| NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
in
let cic_appl_pattern = refresh cic_appl_pattern in
| NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
in
let cic_appl_pattern = refresh cic_appl_pattern in
- basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+ basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
in
GrafiteTypes.Serializer.register#run "interpretation"
basic_eval_interpretation
;;
let eval_interpretation status data=
in
GrafiteTypes.Serializer.register#run "interpretation"
basic_eval_interpretation
;;
let eval_interpretation status data=
basic_eval_alias (mode,diff)
in
GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
basic_eval_alias (mode,diff)
in
GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
let inject_input_notation =
let basic_eval_input_notation (l1,l2)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
let inject_input_notation =
let basic_eval_input_notation (l1,l2)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
- 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_input_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_input_notation (l1,l2) status
+ else
+ status
let inject_output_notation =
let basic_eval_output_notation (l1,l2)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
let inject_output_notation =
let basic_eval_output_notation (l1,l2)
~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
- 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
- let u1 = refresh_uri_in_universe u1 in
- let u2 = refresh_uri_in_universe u2 in
- basic_eval_add_constraint (u1,u2)
+ if not alias_only then
+ let u1 = refresh_uri_in_universe u1 in
+ let u2 = refresh_uri_in_universe u2 in
+ basic_eval_add_constraint (u1,u2) status
+ else
+ status
| GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
| GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
| GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
| GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
| GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
| GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
| GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
| GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
| GrafiteAst.NTry (_,tac) -> NTactics.try_tac
| GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
| GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
| GrafiteAst.NTry (_,tac) -> NTactics.try_tac
| GrafiteAst.NAssumption _ -> NTactics.assumption_tac
| GrafiteAst.NBlock (_,l) ->
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
| GrafiteAst.NAssumption _ -> NTactics.assumption_tac
| GrafiteAst.NBlock (_,l) ->
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
| GrafiteAst.Include (loc, mode, fname) ->
let _root, baseuri, _fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname in
| GrafiteAst.Include (loc, mode, fname) ->
let _root, baseuri, _fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname in
let status = status#set_dump (obj::status#dump) in
let status = status#set_dependencies (fname::status#dependencies) in
let status = status#set_dump (obj::status#dump) in
let status = status#set_dependencies (fname::status#dependencies) in
status
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
status
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->