summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.mli2
-rw-r--r--plugins/subtac/g_subtac.ml42
-rw-r--r--plugins/subtac/subtac.ml2
-rw-r--r--plugins/subtac/subtac_cases.ml6
-rw-r--r--plugins/subtac/subtac_cases.mli2
-rw-r--r--plugins/subtac/subtac_classes.ml2
-rw-r--r--plugins/subtac/subtac_classes.mli2
-rw-r--r--plugins/subtac/subtac_coercion.ml8
-rw-r--r--plugins/subtac/subtac_pretyping.ml4
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml25
10 files changed, 29 insertions, 26 deletions
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index a0b693de..35744b71 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 6e7a8d32..c89d135f 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index ad248bfb..89d9050c 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 0b1ed9bb..9ff8ba50 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -411,7 +411,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
let _ = e_cumul pb.env pb.isevars indt typ in
current
else
- (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
+ (evd_comb2 (Coercion.inh_conv_coerce_to true dummy_loc pb.env)
pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
let sigma = !(pb.isevars) in
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
@@ -1478,7 +1478,7 @@ let extract_arity_signatures env0 tomatchl tmsign =
let inh_conv_coerce_to_tycon loc env isevars j tycon =
match tycon with
| Some p ->
- let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+ let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in
isevars := evd';
j
| None -> j
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 91142067..5ef42b13 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index f11f611f..b0054d82 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 2c9fbaf5..bd3fe484 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 0c03fb4c..4fe29ac8 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -358,7 +358,7 @@ module Coercion = struct
(hj,typ_cl) p)
with e when Errors.noncritical e -> anomaly "apply_coercion"
- let inh_app_fun env isevars j =
+ let inh_app_fun _ env isevars j =
let isevars = ref isevars in
let t = hnf env !isevars j.uj_type in
match kind_of_term t with
@@ -481,8 +481,8 @@ module Coercion = struct
| Some (init, cur) ->
(evd, cj)
- let inh_conv_coerce_to = inh_conv_coerce_to_gen false
- let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+ let inh_conv_coerce_to _ = inh_conv_coerce_to_gen false
+ let inh_conv_coerce_rigid_to _ = inh_conv_coerce_to_gen true
let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
let nabsinit, nabs =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index fac6b567..68636574 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -63,7 +63,7 @@ let my_print_rec_info env t =
(* str " in environment: " ++ my_print_env env); *)
let interp env isevars c tycon =
- let j = pretype tycon env isevars ([],[]) c in
+ let j = pretype true tycon env isevars ([],[]) c in
let _ = isevars := Evarutil.nf_evar_map !isevars in
let evd = consider_remaining_unif_problems env !isevars in
(* let unevd = undefined_evars evd in *)
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index f0579711..3fc35c81 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -87,9 +87,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
done
(* coerce to tycon if any *)
- let inh_conv_coerce_to_tycon loc env evdref j = function
+ let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
| None -> j
- | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
+ | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
let push_rels vars env = List.fold_right push_rel vars env
@@ -188,11 +188,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [( evdref)] and *)
(* the type constraint tycon *)
- let rec pretype (tycon : type_constraint) env evdref lvar c =
+ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar c =
(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *)
(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
(* with _ -> () *)
(* in *)
+ let pretype = pretype resolve_tc in
+ let pretype_type = pretype_type resolve_tc in
+ let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
match c with
| GRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env evdref
@@ -335,7 +338,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| [] -> resj
| c::rest ->
let argloc = loc_of_glob_constr c in
- let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+ let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
@@ -557,7 +560,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref cj tycon
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
- and pretype_type valcon env evdref lvar = function
+ and pretype_type resolve_tc valcon env evdref lvar = function
| GHole loc ->
(match valcon with
| Some v ->
@@ -577,7 +580,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
{ utj_val = e_new_evar evdref env ~src:loc (mkSort s);
utj_type = s})
| c ->
- let j = pretype empty_tycon env evdref lvar c in
+ let j = pretype resolve_tc empty_tycon env evdref lvar c in
let loc = loc_of_glob_constr c in
let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
match valcon with
@@ -592,9 +595,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let c' = match kind with
| OfType exptyp ->
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
- (pretype tycon env evdref lvar c).uj_val
+ (pretype resolve_classes tycon env evdref lvar c).uj_val
| IsType ->
- (pretype_type empty_valcon env evdref lvar c).utj_val
+ (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val
in
if resolve_classes then
(try
@@ -616,14 +619,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let understand_judgment sigma env c =
let evdref = ref (create_evar_defs sigma) in
- let j = pretype empty_tycon env evdref ([],[]) c in
+ let j = pretype true empty_tycon env evdref ([],[]) c in
let evd = consider_remaining_unif_problems env !evdref in
let j = j_nf_evar evd j in
check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
let understand_judgment_tcc evdref env c =
- let j = pretype empty_tycon env evdref ([],[]) c in
+ let j = pretype true empty_tycon env evdref ([],[]) c in
j_nf_evar !evdref j
(* Raw calls to the unsafe inference machine: boolean says if we must
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 04:27:08 +0000