diff options
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 13 | ||||
| -rw-r--r-- | pretyping/classops.mli | 1 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 11 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
6 files changed, 9 insertions, 24 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5a88e62dca..18bb390990 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -21,19 +21,6 @@ open Rawterm (* usage qque peu general: utilise aussi dans record *) -type cte_typ = - | NAM_Section_Variable of variable - | NAM_Constant of constant - | NAM_Inductive of inductive - | NAM_Constructor of constructor - -let cte_of_constr c = match kind_of_term c with - | IsConst sp -> ConstRef sp - | IsMutInd ind_sp -> IndRef ind_sp - | IsMutConstruct cstr_cp -> ConstructRef cstr_cp - | IsVar id -> VarRef (Declare.find_section_variable id) - | _ -> raise Not_found - type cl_typ = | CL_SORT | CL_FUN diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 019644e20a..c68eba1ddf 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -44,7 +44,6 @@ type coe_index (* This is the type of paths from a class to another *) type inheritance_path = coe_index list -val cte_of_constr : constr -> global_reference val coe_of_reference : global_reference -> coe_typ (*s [declare_class] adds a class to the set of declared classes *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b4df53b8a8..e0c1db1690 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -99,12 +99,11 @@ let used_of = global_vars_and_consts (* Tools for printing of Cases *) let encode_inductive ref = - let indsp = - match kind_of_term (constr_of_reference Evd.empty (Global.env()) ref)with - | IsMutInd indsp -> indsp - | _ -> errorlabstrm "indsp_of_id" - [< 'sTR ((Global.string_of_global ref)^ - " is not an inductive type") >] in + let indsp = match ref with + | IndRef indsp -> indsp + | _ -> errorlabstrm "indsp_of_id" + [< 'sTR ((Global.string_of_global ref)^" is not an inductive type") >] + in let mis = Global.lookup_mind_specif indsp in let constr_lengths = Array.map List.length (mis_recarg mis) in (indsp,constr_lengths) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e221e49450..23bcfd8e45 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -310,7 +310,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = and check_conv_record (t1,l1) (t2,l2) = try let {o_DEF=c;o_TABS=bs;o_TPARAMS=xs;o_TCOMPS=us} = - objdef_info (cte_of_constr t1,cte_of_constr t2) in + objdef_info (Declare.reference_of_constr t1, Declare.reference_of_constr t2) in let xs1,t,ts = match list_chop (List.length xs) l1 with | xs1,t::ts -> xs1,t,ts diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 54e67e401c..253e3e579d 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -161,7 +161,7 @@ let matches_core convert pat c = | PVar v1, IsVar v2 when v1 = v2 -> sigma - | PRef ref, _ when Declare.constr_of_reference Evd.empty (Global.env()) ref = cT -> sigma + | PRef ref, _ when Declare.constr_of_reference ref = cT -> sigma | PRel n1, IsRel n2 when n1 = n2 -> sigma @@ -184,7 +184,7 @@ let matches_core convert pat c = | PRef (ConstRef _ as ref), _ when convert <> None -> let (env,evars) = out_some convert in - let c = Declare.constr_of_reference Evd.empty env ref in + let c = Declare.constr_of_reference ref in if is_conv env evars c cT then sigma else raise PatternMatchingFailure diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2cb322bea8..c0238dbdae 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -165,7 +165,7 @@ let pretype_id loc env lvar id = (* Main pretyping function *) let pretype_ref isevars env lvar ref = - let c = Declare.constr_of_reference (evars_of isevars) env ref in + let c = Declare.constr_of_reference ref in make_judge c (Retyping.get_type_of env Evd.empty c) (* |