select_tac ~where ~job:(`Collect l) true;
print_tac true "ha selezionato?";
(fun s -> distribute_tac (fun status goal ->
- if !l = [] then fail (lazy "No term to generalize");
- let goalty = get_goalty status goal in
- let canon = List.hd !l in
- let status =
+ let goalty = get_goalty status goal in
+ let status,canon,rest =
+ match !l with
+ [] ->
+ (match where with
+ _,_,(None,_,_) -> fail (lazy "No term to generalize")
+ | txt,txtlen,(Some what,_,_) ->
+ let status, what =
+ disambiguate status (txt,txtlen,what) None (ctx_of goalty)
+ in
+ status,what,[]
+ )
+ | he::tl -> status,he,tl in
+ let status =
List.fold_left
- (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l)
- in
- let status, canon = term_of_cic_term status canon (ctx_of goalty) in
- instantiate status goal
- (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
+ (fun s t -> unify s (ctx_of goalty) canon t) status rest in
+ let status, canon = term_of_cic_term status canon (ctx_of goalty) in
+ instantiate status goal
+ (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
) s) ]
;;
-let eval_tac ~reduction ~where =
+let reduce_tac ~reduction ~where =
let change status t =
match reduction with
+ | `Normalize perform_delta ->
+ normalize status
+ ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
| `Whd perform_delta ->
- whd status
- ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
+ whd status
+ ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
in
let where = GrafiteDisambiguate.disambiguate_npattern where in
select0_tac ~where ~job:(`ChangeWith change)