module C = Cic
module E = CicEnvironment
module Un = CicUniv
-module TC = CicTypeChecker
-module D = Deannotate
+module TC = CicTypeChecker
module UM = UriManager
module Rd = CicReduction
module PEH = ProofEngineHelpers
module PT = PrimitiveTactics
-
module DTI = DoubleTypeInference
-(* helpers ******************************************************************)
+module H = ProceduralHelpers
-let cic = D.deannotate_term
+(* helpers ******************************************************************)
let rec list_sub start length = function
| _ :: tl when start > 0 -> list_sub (pred start) length tl
| C.ALambda (_, _, _, t) when n > 0 ->
aux 0 (pred n) (lift 1 (-1) t)
| t when n > 0 ->
- Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+ Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
assert false
| t -> t
in
aux [] c
let elim_inferred_type context goal arg using cpattern =
- let metasenv, ugraph = [], Un.oblivion_ugraph in
- let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+ let metasenv, ugraph = [], Un.default_ugraph in
+ let ety = H.get_type "elim_inferred_type" context using in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim
~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no