| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;
-module CicHash =
- struct
- module Tmp =
- Hashtbl.Make
- (struct
- type t = Cic.term
- let equal = (==)
- let hash = Hashtbl.hash
- end)
- include Tmp
- let empty () = Tmp.create 1
- end
-;;
-
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
let rec type_of_aux' subterms_to_types metasenv context t expectedty =
(* Coscoy's double type-inference algorithm *)
{synthesized = synthesized' ; expected = Some expectedty'},
expectedty'
in
- assert (not (CicHash.mem subterms_to_types t));
- CicHash.add subterms_to_types t types ;
+ assert (not (Cic.CicHash.mem subterms_to_types t));
+ Cic.CicHash.add subterms_to_types t types ;
res
and visit_exp_named_subst context uri exp_named_subst =
;;
let double_type_of metasenv context t expectedty =
- let subterms_to_types = CicHash.create 503 in
+ let subterms_to_types = Cic.CicHash.create 503 in
ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
subterms_to_types
;;