| `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 =