diff options
author | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
commit | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (patch) | |
tree | 8b5450c5801a1592e0348ad0362f950e7bb958d4 /plugins/subtac | |
parent | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (diff) |
Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg
Diffstat (limited to 'plugins/subtac')
-rw-r--r-- | plugins/subtac/eterm.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/g_subtac.ml4 | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac.ml | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.ml | 6 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 8 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 4 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 25 |
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 |