* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
(DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
-let find_in_context name (context: Cic.name list) =
+let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
| Cic.Name hd :: tl when hd = name -> acc
where_dom @ defs_dom
| CicNotationPt.Ident (name, subst) ->
(try
- let index = find_in_context name context in
+ (* the next line can raise Not_found *)
+ ignore(find_in_context name context);
if subst <> None then
CicNotationPt.fail loc "Explicit substitutions not allowed here"
else
List.flatten
(List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
let dom =
+ List.fold_left
+ (fun dom (_,ty) ->
+ domain_rev_of_term [] ty @ dom
+ ) (dom @ domain_rev_of_term [] ty) params
+ in
List.filter
(fun name->
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_) -> name = Id name') fields)
) dom
- in
- List.fold_left
- (fun dom (_,ty) ->
- domain_rev_of_term [] ty @ dom
- ) (dom @ domain_rev_of_term [] ty) params
in
rev_uniq domain_rev