* http://helm.cs.unibo.it/
*)
+open Printf
+
open CicNotationEnv
open CicNotationPt
| _ -> assert false
in
instantiate_fold_right env)
- | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t))
+ | If (_, p_true, p_false) as t ->
+ aux env (CicNotationUtil.find_branch (Magic t))
| Fail -> assert false
| _ -> assert false
in
aux env term
+let instantiate_appl_pattern env appl_pattern =
+ let lookup name =
+ try List.assoc name env
+ with Not_found ->
+ prerr_endline (sprintf "Name %s not found" name);
+ assert false
+ in
+ let rec aux = function
+ | UriPattern uri -> CicUtil.term_of_uri uri
+ | ImplicitPattern -> Cic.Implicit None
+ | VarPattern name -> lookup name
+ | ApplPattern terms -> Cic.Appl (List.map aux terms)
+ in
+ aux appl_pattern
+