diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extraction.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml4 | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index e1848589d6..4888c8fefb 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -671,12 +671,12 @@ let extract_constant kn r = | (Info, Arity) -> let s,vl = type_sign_vl env typ in let db = db_from_sign s in - let body = Lazy.force_val l_body in + let body = Declarations.force l_body in let t = extract_type_arity env db body (List.length s) in Dtype (r, vl, t) | (Logic, _) -> Dterm (r, MLdummy') | (Info, _) -> - let body = Lazy.force_val l_body in + let body = Declarations.force l_body in let a = extract_term env body in if a <> MLdummy' then Dterm (r, kill_prop_lams_eta a (signature_of_kn kn)) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index b35a5f56fa..0ae3b2d821 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -177,7 +177,7 @@ let constant_to_ast_list kn = None -> make_variable_ast (id_of_label (label kn)) typ l | Some c1 -> - make_definition_ast (id_of_label (label kn)) (Lazy.force_val c1) typ l) + make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = let ((id, c, v), _) = get_variable sp in diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4 index 8710a9e1fa..5ca89dd3f1 100644 --- a/contrib/xml/xmlcommand.ml4 +++ b/contrib/xml/xmlcommand.ml4 @@ -740,7 +740,7 @@ let print (_,qid as locqid) fn = match val0 with None -> print_axiom id typ [] hyps env inner_types | Some lc -> - let c = Lazy.force_val lc in + let c = Declarations.force lc in print_definition id c typ [] hyps env inner_types end | Ln.IndRef (kn,_) -> @@ -859,7 +859,7 @@ let print_object lobj id (sp,kn) dn fv env = match val0 with None -> print_axiom id typ fv hyps env inner_types | Some lc -> - let c = Lazy.force_val lc in + let c = Declarations.force lc in print_definition id c typ fv hyps env inner_types end | "INDUCTIVE" -> |