| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
- | `Unfold what -> Tactics.unfold ~pattern ?what
+ | `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
status, GrafiteAst.Obj (loc,obj)
let make_absolute paths path =
- let rec aux = function
- | [] -> ignore (Unix.stat path); path
- | p :: tl ->
- let path = p ^ "/" ^ path in
- try
- ignore (Unix.stat path); path
- with Unix.Unix_error _ -> aux tl
- in
- try
- aux paths
- with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
+ if path = "coq.ma" then path
+ else
+ let rec aux = function
+ | [] -> ignore (Unix.stat path); path
+ | p :: tl ->
+ let path = p ^ "/" ^ path in
+ try
+ ignore (Unix.stat path); path
+ with Unix.Unix_error _ -> aux tl
+ in
+ try
+ aux paths
+ with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
;;
let eval_command opts status cmd =
eval_coercion status coercion
| GrafiteAst.Alias (loc, spec) ->
let aliases =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
DisambiguateTypes.Environment.add