From 152f57925a6dc08ce3f332319b50eae9fb7bb622 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 24 Feb 2015 18:44:20 +0100
Subject: Calling coq references lazily in plugin cc so as to support static
 linking of plugins.

---
 plugins/cc/cctac.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7110e5b23..8884aef1c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,7 +23,7 @@ open Pp
 open Errors
 open Util
 
-let reference dir s = Coqlib.gen_reference "CC" dir s
+let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
 let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -91,7 +91,7 @@ let atom_of_constr env sigma term =
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -126,7 +126,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -147,7 +147,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -159,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -246,10 +246,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k = 
-  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k = 
-  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
@@ -375,9 +375,9 @@ let discriminate_tac (cstr,u as cstru) p =
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
-    let identity = Universes.constr_of_global _I in
+    let identity = Universes.constr_of_global (Lazy.force _I) in
     (* let trivial=pf_type_of gls identity in *)
-    let trivial = Universes.constr_of_global _True in
+    let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
@@ -493,7 +493,7 @@ let f_equal =
     in
     Proofview.tclORELSE
       begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
+      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
 	  begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
-- 
cgit v1.2.3