summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml2
-rw-r--r--pretyping/arguments_renaming.mli2
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/cases.mli2
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/cbv.mli2
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.ml24
-rw-r--r--pretyping/coercion.mli20
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--pretyping/evarconv.ml20
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarutil.ml37
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/evd.ml2
-rw-r--r--pretyping/evd.mli2
-rw-r--r--pretyping/glob_term.ml23
-rw-r--r--pretyping/glob_term.mli2
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/indrec.mli2
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/matching.ml2
-rw-r--r--pretyping/matching.mli2
-rw-r--r--pretyping/namegen.ml2
-rw-r--r--pretyping/namegen.mli2
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/pattern.mli2
-rw-r--r--pretyping/pretype_errors.ml2
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--pretyping/pretyping.ml43
-rw-r--r--pretyping/pretyping.mli6
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/tacred.mli2
-rw-r--r--pretyping/term_dnet.ml2
-rw-r--r--pretyping/term_dnet.mli2
-rw-r--r--pretyping/termops.ml2
-rw-r--r--pretyping/termops.mli2
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typeclasses_errors.ml2
-rw-r--r--pretyping/typeclasses_errors.mli2
-rw-r--r--pretyping/typing.ml2
-rw-r--r--pretyping/typing.mli2
-rw-r--r--pretyping/unification.ml4
-rw-r--r--pretyping/unification.mli2
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--pretyping/vnorm.mli2
56 files changed, 151 insertions, 126 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 92378837..78290e03 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.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/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a4121623..74c4cdc3 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.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/pretyping/cases.ml b/pretyping/cases.ml
index 38355cf1..57857351 100644
--- a/pretyping/cases.ml
+++ b/pretyping/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 *)
@@ -391,7 +391,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
let _ = e_cumul pb.env pb.evdref 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.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
let sigma = !(pb.evdref) in
(current,try_find_ind pb.env sigma indt names))
@@ -1680,7 +1680,7 @@ let extract_arity_signature env0 tomatchl tmsign =
let inh_conv_coerce_to_tycon loc env evdref j tycon =
match tycon with
| Some p ->
- let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in
+ let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
evdref := evd';
j
| None -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 566c172d..826d68a4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/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/pretyping/cbv.ml b/pretyping/cbv.ml
index 9429086c..08ec25be 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.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/pretyping/cbv.mli b/pretyping/cbv.mli
index 08e52ff7..eb0abe97 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.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/pretyping/classops.ml b/pretyping/classops.ml
index ddc99e0e..59f3c740 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.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/pretyping/classops.mli b/pretyping/classops.mli
index 675ccbbc..0136b90c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.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/pretyping/coercion.ml b/pretyping/coercion.ml
index 86f96c7c..917856a2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/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 *)
@@ -36,7 +36,7 @@ module type S = sig
inserts a coercion into [j], if needed, in such a way it gets as
type a product; it returns [j] if no coercion is applicable *)
val inh_app_fun :
- env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+ bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
(* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
@@ -57,10 +57,10 @@ module type S = sig
(* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
- val inh_conv_coerce_to : loc ->
+ val inh_conv_coerce_to : bool -> loc ->
env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
- val inh_conv_coerce_rigid_to : loc ->
+ val inh_conv_coerce_rigid_to : bool -> loc ->
env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
(* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
@@ -140,9 +140,11 @@ module Default = struct
lookup_path_to_fun_from env evd j.uj_type in
(evd,apply_coercion env evd p j t)
- let inh_app_fun env evd j =
+ let inh_app_fun resolve_tc env evd j =
try inh_app_fun env evd j
- with Not_found ->
+ with
+ | Not_found when not resolve_tc -> (evd, j)
+ | Not_found ->
try inh_app_fun env (saturate_evd env evd) j
with Not_found -> (evd, j)
@@ -221,13 +223,15 @@ module Default = struct
| _ -> raise NoCoercion
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
+ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj (n, t) =
match n with
None ->
let (evd', val') =
try
inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
+ with
+ | NoCoercion when not resolve_tc -> error_actual_type_loc loc env evd cj t
+ | NoCoercion ->
let evd = saturate_evd env evd in
try
inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
@@ -238,8 +242,8 @@ module Default = struct
(evd',{ uj_val = val'; uj_type = t })
| 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 resolve_tc = inh_conv_coerce_to_gen resolve_tc false
+ let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') =
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 4c4725b3..f06f58f4 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.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 *)
@@ -18,11 +18,13 @@ open Glob_term
module type S = sig
(** {6 Coercions. } *)
- (** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+ (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
- type a product; it returns [j] if no coercion is applicable *)
+ type a product; it returns [j] if no coercion is applicable.
+ resolve_tc=false disables resolving type classes (as the last
+ resort before failing) *)
val inh_app_fun :
- env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+ bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
(** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
@@ -40,13 +42,15 @@ module type S = sig
val inh_coerce_to_prod : loc ->
env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
- (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
+ (** [inh_conv_coerce_to resolve_tc loc env isevars j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
- [j.uj_type] are convertible; it fails if no coercion is applicable *)
- val inh_conv_coerce_to : loc ->
+ [j.uj_type] are convertible; it fails if no coercion is applicable.
+ resolve_tc=false disables resolving type classes (as the last
+ resort before failing) *)
+ val inh_conv_coerce_to : bool -> loc ->
env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
- val inh_conv_coerce_rigid_to : loc ->
+ val inh_conv_coerce_rigid_to : bool -> loc ->
env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1065aec9..9e808dd4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.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/pretyping/detyping.mli b/pretyping/detyping.mli
index cd017ba7..bbd94cfe 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.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/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f0019448..8b421ea3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.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 *)
@@ -20,6 +20,17 @@ open Evarutil
open Libnames
open Evd
+let debug_unification = ref (false)
+let _ = Goptions.declare_bool_option {
+ Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optname =
+ "Print states sended to Evarconv unification";
+ Goptions.optkey = ["Debug";"Unification"];
+ Goptions.optread = (fun () -> !debug_unification);
+ Goptions.optwrite = (fun a -> debug_unification:=a);
+}
+
+
type flex_kind_of_term =
| Rigid of constr
| PseudoRigid of constr (* approximated as rigid but not necessarily so *)
@@ -210,6 +221,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
in
(* Evar must be undefined since we have flushed evars *)
+ let () = if !debug_unification then
+ let open Pp in
+ let pr_state (tm,l) =
+ h 0 (Termops.print_constr tm ++ str "|" ++ cut ()
+ ++ prlist_with_sep pr_semicolon
+ (fun x -> hov 1 (Termops.print_constr x)) l) in
+ pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in
match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index dd68f16f..3a352d13 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.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/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fc29ba6c..05b7e443 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.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 *)
@@ -1180,17 +1180,28 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
* such that "hyps' |- ?e : T"
*)
-let filter_candidates evd evk filter candidates =
+let filter_effective_candidates evi filter candidates =
+ match filter with
+ | None -> candidates
+ | Some filter ->
+ let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
+ List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids)
+ candidates
+
+let filter_candidates evd evk filter candidates_update =
let evi = Evd.find_undefined evd evk in
- let candidates = match candidates with
+ let candidates = match candidates_update with
| None -> evi.evar_candidates
- | Some _ -> candidates in
- match candidates,filter with
- | None,_ | _, None -> candidates
- | Some l, Some filter ->
- let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
- Some (List.filter (fun a ->
- list_subset (Idset.elements (collect_vars a)) ids) l)
+ | Some _ -> candidates_update
+ in
+ match candidates with
+ | None -> None
+ | Some l ->
+ let l' = filter_effective_candidates evi filter l in
+ if List.length l = List.length l' && candidates_update = None then
+ None
+ else
+ Some l'
let closure_of_filter evd evk filter =
let evi = Evd.find_undefined evd evk in
@@ -1530,6 +1541,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress of (identifier * evar_projection) list
+exception NotEnoughInformationEvarEvar of constr
exception OccurCheckIn of evar_map * constr
let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
@@ -1608,7 +1620,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
with
| EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
| CannotProject filter' ->
- assert !progress;
+ if not !progress then
+ raise (NotEnoughInformationEvarEvar t);
(* Make the virtual left evar real *)
let ty = get_type_of env' !evdref t in
let (evd,evar'',ev'') =
@@ -1714,6 +1727,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
with
| NotEnoughInformationToProgress sols ->
postpone_non_unique_projection env evd ev sols rhs
+ | NotEnoughInformationEvarEvar t ->
+ add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd
| NotInvertibleUsingOurAlgorithm t ->
error_not_clean env evd evk t (evar_source evk evd)
| OccurCheckIn (evd,rhs) ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 591a008c..9269f138 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.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/pretyping/evd.ml b/pretyping/evd.ml
index 4d9eb897..72dc27e6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.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/pretyping/evd.mli b/pretyping/evd.mli
index dbaf803b..d5bf2f68 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.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/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 8e4b211f..b7023db0 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.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 *)
@@ -359,27 +359,6 @@ let rec cases_pattern_of_glob_constr na = function
PatCstr (loc,cstr,args,na)
| _ -> raise Not_found
-let rec cases_pattern_of_glob_constr na = function
- | GVar (loc,id) when na<>Anonymous ->
- (* Unable to manage the presence of both an alias and a variable *)
- raise Not_found
- | GVar (loc,id) -> PatVar (loc,Name id)
- | GHole (loc,_) -> PatVar (loc,na)
- | GRef (loc,ConstructRef cstr) ->
- PatCstr (loc,cstr,[],na)
- | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
- let mib,_ = Global.lookup_inductive ind in
- let nparams = mib.Declarations.mind_nparams in
- if nparams > List.length args then
- user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
- let params,args = list_chop nparams args in
- List.iter (function GHole _ -> ()
- | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
- params;
- let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
- PatCstr (loc,cstr,args,na)
- | _ -> raise Not_found
-
(* Turn a closed cases pattern into a glob_constr *)
let rec glob_constr_of_closed_cases_pattern_aux = function
| PatCstr (loc,cstr,[],Anonymous) ->
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index 798a960f..09dd9203 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.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/pretyping/indrec.ml b/pretyping/indrec.ml
index 18d30bfd..c7cdb302 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.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/pretyping/indrec.mli b/pretyping/indrec.mli
index 1bf5fd90..19c70dc0 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.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/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bdccc57b..5bfc57bf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.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/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 91662fd9..133d7013 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.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/pretyping/matching.ml b/pretyping/matching.ml
index d99b8c9f..b86f3e45 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.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/pretyping/matching.mli b/pretyping/matching.mli
index 9b412692..1a47b714 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.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/pretyping/namegen.ml b/pretyping/namegen.ml
index e5dd75c0..76b9bd8a 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.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/pretyping/namegen.mli b/pretyping/namegen.mli
index e23c6dad..db078026 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.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/pretyping/pattern.ml b/pretyping/pattern.ml
index 7e486956..553615c2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.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/pretyping/pattern.mli b/pretyping/pattern.mli
index f6d55bc6..7fb53133 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.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/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 672debfa..52122974 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.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/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 68ea67f7..75962d11 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.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/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
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 761e1641..a785b432 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.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 *)
@@ -93,11 +93,11 @@ sig
(**/**)
(** Internal of Pretyping... *)
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 :
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 434fe80c..f9cd3501 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.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/pretyping/recordops.mli b/pretyping/recordops.mli
index 1c19ef6c..442e51db 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.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/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 993ad46b..7c348d97 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.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/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6f7f9de3..f508ea6c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.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/pretyping/retyping.ml b/pretyping/retyping.ml
index 3f6acfcb..1e1960f5 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.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/pretyping/retyping.mli b/pretyping/retyping.mli
index 62bda6ef..4ef54c13 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.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/pretyping/tacred.ml b/pretyping/tacred.ml
index 78b239c0..b18314f7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.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/pretyping/tacred.mli b/pretyping/tacred.mli
index f2a4c303..aec9da95 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.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/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 3340dbe2..28a6c92c 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.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/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index bf4557fc..9e629dcd 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.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/pretyping/termops.ml b/pretyping/termops.ml
index 0e31ee2d..02661a93 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.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/pretyping/termops.mli b/pretyping/termops.mli
index 0e384829..81b23d7e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.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/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0344ebcc..2b5b7fe2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.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/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c458e5d5..91069b70 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.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/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 19e18489..da5dc909 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.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/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index cb67c73d..6e0fc6ad 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.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/pretyping/typing.ml b/pretyping/typing.ml
index 22aacb29..9fbfc197 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.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/pretyping/typing.mli b/pretyping/typing.mli
index 88dc895e..5aa0a2d4 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.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/pretyping/unification.ml b/pretyping/unification.ml
index fd045690..d6b1e2e4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.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 *)
@@ -794,7 +794,7 @@ let is_mimick_head ts f =
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
- let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+ let (evd',j') = inh_conv_coerce_rigid_to true dummy_loc env evd j tycon in
let evd' = Evarconv.consider_remaining_unif_problems env evd' in
let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
(evd',j'.uj_val)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 1ec5c1a2..75bddc1f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.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/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3966146d..047971d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.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/pretyping/vnorm.mli b/pretyping/vnorm.mli
index ca370b55..a0cf2372 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.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 *)