diff options
Diffstat (limited to 'pretyping')
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 *) |