diff options
| -rw-r--r-- | contrib/dp/dp.ml | 6 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/cic2acic.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | library/libnames.ml | 3 | ||||
| -rw-r--r-- | library/libnames.mli | 9 | ||||
| -rw-r--r-- | parsing/g_zsyntax.ml | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 | ||||
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
10 files changed, 18 insertions, 16 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 24744e768..9dc538c78 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -159,7 +159,7 @@ let rec tr_type env ty = end | _ -> assert false end - else let r = reference_of_constr ty in + else let r = global_of_constr ty in try begin match lookup_global r with | DeclType id -> [], id @@ -295,7 +295,7 @@ and tr_term bv env t = | _ -> let f, cl = decompose_app t in begin try - let r = reference_of_constr f in + let r = global_of_constr f in match tr_global env r with | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term bv env) cl) @@ -351,7 +351,7 @@ and tr_formula bv env f = assert false (* TODO Exists (tr_formula bv env a) *) | _ -> begin try - let r = reference_of_constr c in + let r = global_of_constr c in match tr_global env r with | DeclPred (s, _) -> Fatom (Pred (s, List.map (tr_term bv env) args)) diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 90defda9c..657d4cba5 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -269,7 +269,7 @@ let create_with_auto_hints l depth gl= Res_pf (c,_) | Give_exact c | Res_pf_THEN_trivial_fail (c,_) -> (try - let gr=reference_of_constr c in + let gr=global_of_constr c in let typ=(pf_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 10a428e83..a0faa6426 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -468,7 +468,7 @@ print_endline "PASSATO" ; flush stdout ; let subst,residual_args,uninst_vars = let variables,basedir = try - let g = Libnames.reference_of_constr h in + let g = Libnames.global_of_constr h in let sp = match g with Libnames.ConstructRef ((induri,_),_) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3a9dc3a75..89d4e57ae 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -530,7 +530,7 @@ let find_constructor ref = let rec unf = function | ConstRef cst -> let v = Environ.constant_value (Global.env()) cst in - unf (reference_of_constr v) + unf (global_of_constr v) | ConstructRef c -> if !dump then add_glob loc r; c, [] diff --git a/library/libnames.ml b/library/libnames.ml index 361c01696..b7ec0c223 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -34,7 +34,7 @@ let subst_global subst ref = match ref with if kn==kn' then ref, mkConstruct ((kn,i),j) else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j) -let reference_of_constr c = match kind_of_term c with +let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp | Ind ind_sp -> IndRef ind_sp | Construct cstr_cp -> ConstructRef cstr_cp @@ -48,6 +48,7 @@ let constr_of_global = function | IndRef sp -> mkInd sp let constr_of_reference = constr_of_global +let reference_of_constr = global_of_constr module RefOrdered = struct diff --git a/library/libnames.mli b/library/libnames.mli index 43e31d08f..a9051623f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -28,11 +28,12 @@ val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) val constr_of_global : global_reference -> constr -(* Obsolete synonym for constr_of_global *) -val constr_of_reference : global_reference -> constr +(* Turn a construction denoting a global reference into a global reference; + raise [Not_found] if not a global reference *) +val global_of_constr : constr -> global_reference -(* Turn a construction denoting a global into a reference; - raise [Not_found] if not a global *) +(* Obsolete synonyms for constr_of_global and global_of_constr *) +val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference module Refset : Set.S with type elt = global_reference diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 9ca72e18a..82e651b4e 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -86,7 +86,7 @@ exception Non_closed_number let get_z_sign_ast loc = let ast_of_id id = Termast.ast_of_ref - (reference_of_constr + (global_of_constr (gen_constant_in_modules "Z-printer" zarith_base_modules id)) in ((ast_of_id "xI", diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 47d468bd3..6da2c8c2f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -79,7 +79,7 @@ let make_flag f = in red let is_reference c = - try let r = reference_of_constr c in true with _ -> false + try let r = global_of_constr c in true with _ -> false let red_expr_tab = ref Stringmap.empty diff --git a/tactics/auto.ml b/tactics/auto.ml index ea7c62a1c..0fda09a9a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -423,7 +423,7 @@ let add_hints local dbnames0 h = let f (n,c) = let c = Constrintern.interp_constr sigma env c in let n = match n with - | None -> (*id_of_global (reference_of_constr c)*) + | None -> (*id_of_global (global_of_constr c)*) id_of_string "<anonymous hint>" | Some n -> n in (n,c) in @@ -433,7 +433,7 @@ let add_hints local dbnames0 h = let f (n,c) = let c = Constrintern.interp_constr sigma env c in let n = match n with - | None -> (*id_of_global (reference_of_constr c)*) + | None -> (*id_of_global (global_of_constr c)*) id_of_string "<anonymous hint>" | Some n -> n in (n,c) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 198a17bcd..0216b3b65 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1465,7 +1465,7 @@ let compute_elim_signature elimt names_info = error_ind_scheme "the conclusion of"; let indhd,indargs = decompose_app ind in let indt = - try reference_of_constr indhd + try global_of_constr indhd with _ -> error "Cannot find the inductive type of the inductive schema" in let nparams = List.length indargs - nrealargs in let revparams, revhyps2 = chop_context nparams (List.rev hyps1) in |