let newgoalty = mk_cic_term newgoalctx newgoalty in
let status, instance =
- mk_meta status newgoalctx (`Decl newgoalty)
+ mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
in
instantiate status goal instance)
;;
let l = ref [] in
block_tac [
select_tac ~where ~job:(`Collect l) true;
- print_tac true "ha selezionato?";
(fun s -> distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status,canon,rest =
block_tac [
exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
branch_tac;
- pos_tac [2]; exact_tac t;
- shift_tac; pos_tac [1]; skip_tac;
+ pos_tac [3]; exact_tac t;
+ shift_tac; pos_tac [2]; skip_tac;
merge_tac ]
;;
let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status,sort = typeof status (ctx_of goalty) goalty in
- let sort = fix_sorts sort in
+ let status, sort = fix_sorts status sort in
let status, sort = term_of_cic_term status sort (ctx_of goalty) in
sortref := sort;
status)