summaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml37
1 files changed, 23 insertions, 14 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 504d01af..ddc99e0e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: classops.ml 14776 2011-12-07 17:54:28Z herbelin $ *)
-
open Util
open Pp
open Flags
@@ -19,7 +17,7 @@ open Libobject
open Library
open Term
open Termops
-open Rawterm
+open Glob_term
open Decl_kinds
open Mod_subst
@@ -48,6 +46,13 @@ type coe_info_typ = {
coe_is_identity : bool;
coe_param : int }
+let coe_info_typ_equal c1 c2 =
+ eq_constr c1.coe_value c2.coe_value &&
+ eq_constr c1.coe_type c2.coe_type &&
+ c1.coe_strength = c2.coe_strength &&
+ c1.coe_is_identity = c2.coe_is_identity &&
+ c1.coe_param = c2.coe_param
+
type cl_index = int
type coe_index = coe_info_typ
@@ -134,9 +139,9 @@ let coercion_info coe = Gmap.find coe !coercion_tab
let coercion_exists coe = Gmap.mem coe !coercion_tab
-(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
+(* find_class_type : evar_map -> constr -> cl_typ * constr list *)
-let find_class_type env sigma t =
+let find_class_type sigma t =
let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
match kind_of_term t' with
| Var id -> CL_SECVAR id, args
@@ -154,7 +159,7 @@ let subst_cl_typ subst ct = match ct with
| CL_CONST kn ->
let kn',t = subst_con subst kn in
if kn' == kn then ct else
- fst (find_class_type (Global.env()) Evd.empty t)
+ fst (find_class_type Evd.empty t)
| CL_IND (kn,i) ->
let kn' = subst_ind subst kn in
if kn' == kn then ct else
@@ -169,12 +174,12 @@ let subst_coe_typ subst t = fst (subst_global subst t)
let class_of env sigma t =
let (t, n1, i, args) =
try
- let (cl,args) = find_class_type env sigma t in
+ let (cl,args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, args)
with Not_found ->
let t = Tacred.hnf_constr env sigma t in
- let (cl, args) = find_class_type env sigma t in
+ let (cl, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, args)
in
@@ -182,7 +187,7 @@ let class_of env sigma t =
let inductive_class_of ind = fst (class_info (CL_IND ind))
-let class_args_of env sigma c = snd (find_class_type env sigma c)
+let class_args_of env sigma c = snd (find_class_type sigma c)
let string_of_class = function
| CL_FUN -> "Funclass"
@@ -211,14 +216,14 @@ let lookup_path_to_sort_from_class s =
let apply_on_class_of env sigma t cont =
try
- let (cl,args) = find_class_type env sigma t in
+ let (cl,args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if List.length args <> n1 then raise Not_found;
t, cont i
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
let t = Tacred.hnf_constr env sigma t in
- let (cl, args) = find_class_type env sigma t in
+ let (cl, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if List.length args <> n1 then raise Not_found;
t, cont i
@@ -308,7 +313,7 @@ let add_coercion_in_graph (ic,source,target) =
try_add_new_path1 (s,target) (p@[ic]);
Gmap.iter
(fun (u,v) q ->
- if u<>v & (u = target) & (p <> q) then
+ if u<>v & u = target && not (list_equal coe_info_typ_equal p q) then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
@@ -344,6 +349,7 @@ open Goptions
let _ =
declare_bool_option
{ optsync = true;
+ optdepr = false;
optname = "automatic import of coercions";
optkey = ["Automatic";"Coercions";"Import"];
optread = (fun () -> !automatically_import_coercions);
@@ -400,7 +406,10 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
if stre = Local then Dispose else Substitute obj
-let (inCoercion,_) =
+type coercion_obj =
+ coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int
+
+let inCoercion : coercion_obj -> obj =
declare_object {(default_object "COERCION") with
open_function = open_coercion;
load_function = load_coercion;