snapshot, notably:

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 436a40571759135d13aa562c0f6bf8518d6f9057..15947f3f238b00d0f9ad875c221f04e3a2e0127a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -244,12 +244,8 @@ let ast_of_acic0 term_info acic k =
 let level1_patterns21 = Hashtbl.create 211
 let level2_patterns32 = Hashtbl.create 211
 
-let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option)
-option ref) =
-  ref None
-let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option)
-option ref) =
-  ref None
+let compiled21 = ref None
+let compiled32 = ref None
 
 let pattern21_matrix = ref []
 let pattern32_matrix = ref []
@@ -257,11 +253,11 @@ let pattern32_matrix = ref []
 let get_compiled21 () =
   match !compiled21 with
   | None -> assert false
-  | Some f -> f
+  | Some f -> Lazy.force f
 let get_compiled32 () =
   match !compiled32 with
   | None -> assert false
-  | Some f -> f
+  | Some f -> Lazy.force f
 
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
@@ -371,7 +367,7 @@ let rec pp_ast1 term =
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
-    | Ast.IdentArg (n, name) ->
+    | GrafiteAst.IdentArg (n, name) ->
         let t = (try List.assoc name env with Not_found -> assert false) in
         let rec count_lambda = function
           | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
@@ -408,10 +404,10 @@ let rec ast_of_acic1 term_info annterm =
       | _ -> Ast.AttributedTerm (`Href uris, ast)
 
 let load_patterns32 t =
-  set_compiled32 (CicNotationMatcher.Matcher32.compiler t)
+  set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
 
 let load_patterns21 t =
-  set_compiled21 (CicNotationMatcher.Matcher21.compiler t)
+  set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
 
 let ast_of_acic id_to_sort annterm =
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in