| GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
+ | `Demodulate ->
+ GrafiteTypes.command_error "demodulation can't be folded"
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
- | `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
- | `Simpl -> Tactics.simpl ~pattern
- | `Unfold what -> Tactics.unfold ~pattern what
- | `Whd -> Tactics.whd ~pattern)
+ | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
+ | `Normalize -> Tactics.normalize ~pattern
+ | `Reduce -> Tactics.reduce ~pattern
+ | `Simpl -> Tactics.simpl ~pattern
+ | `Unfold what -> Tactics.unfold ~pattern what
+ | `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
| GrafiteAst.Replace (_, pattern, with_what) ->
Tactics.replace ~pattern ~with_what
let eval_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
+ prerr_endline "evaluating a coercion command";
GrafiteSync.add_coercion ~basedir ~add_composites status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
None)
lemmas)
in
+ prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
coercions;
- let status = GrafiteTypes.add_moo_content moo_content status in
- let basedir = Helm_registry.get "matita.basedir" in
- List.fold_left
- (fun (status,lemmas) uri ->
- let status,new_lemmas =
- GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
- in
- status,new_lemmas@lemmas
- ) (status,[]) coercions
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ {status with
+ GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
+ lemmas
let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in