summaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2014-07-27 10:02:38 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2014-07-27 10:02:38 +0200
commit420f78b2caeaaddc6fe484565b2d0e49c66888e5 (patch)
tree8b5450c5801a1592e0348ad0362f950e7bb958d4 /pretyping/pretyping.ml
parentd2c5c5e616a6e118291fe1ce9965c731adac03a8 (diff)
Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml43
1 files changed, 24 insertions, 19 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1dd71fab..08e8df05 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/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 *)
@@ -200,11 +200,11 @@ sig
* Unused outside, but useful for debugging
*)
val pretype :
- type_constraint -> env -> evar_map ref ->
+ bool -> type_constraint -> env -> evar_map ref ->
ltac_var_map -> glob_constr -> unsafe_judgment
val pretype_type :
- val_constraint -> env -> evar_map ref ->
+ bool -> val_constraint -> env -> evar_map ref ->
ltac_var_map -> glob_constr -> unsafe_type_judgment
val pretype_gen :
@@ -259,9 +259,9 @@ module Pretyping_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
@@ -297,18 +297,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let c = substl subst c in
{ uj_val = c; uj_type = protected_get_type_of env sigma c }
with Not_found ->
- (* Check if [id] is a section or goal variable *)
- try
- let (_,_,typ) = lookup_named id env in
- { uj_val = mkVar id; uj_type = typ }
- with Not_found ->
- (* [id] not found, build nice error message if [id] yet known from ltac *)
+ (* if [id] an ltac variable not bound to a term *)
+ (* build a nice error message *)
try
match List.assoc id unbndltacvars with
| None -> user_err_loc (loc,"",
str "Variable " ++ pr_id id ++ str " should be bound to a term.")
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
with Not_found ->
+ (* Check if [id] is a section or goal variable *)
+ try
+ let (_,_,typ) = lookup_named id env in
+ { uj_val = mkVar id; uj_type = typ }
+ with Not_found ->
(* [id] not found, standard error message *)
error_var_not_found_loc loc id
@@ -346,7 +347,11 @@ module Pretyping_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 = function
+ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
+ 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 t with
| GRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_ref loc evdref env ref)
@@ -459,7 +464,7 @@ module Pretyping_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) ->
@@ -696,7 +701,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
in 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 ->
@@ -716,7 +721,7 @@ module Pretyping_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
@@ -731,9 +736,9 @@ module Pretyping_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
resolve_evars env evdref fail_evar resolve_classes;
let c = if expand_evar then nf_evar !evdref c' else c' in
@@ -747,14 +752,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let understand_judgment sigma env c =
let evdref = ref sigma in
- let j = pretype empty_tycon env evdref ([],[]) c in
+ let j = pretype true empty_tycon env evdref ([],[]) c in
resolve_evars env evdref true true;
let j = j_nf_evar !evdref j in
check_evars env sigma !evdref (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
resolve_evars env evdref false true;
j_nf_evar !evdref j