From ce6bbd05b7d741750228956a7e045cb202ec0e74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Apr 2015 18:41:09 +0200 Subject: Some dead code. --- pretyping/evarconv.ml | 7 ------- 1 file changed, 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f388f90057..97b1b16455 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -201,13 +201,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -(* This function requires to get the outermost arguments first. It is - a fold_right for backward compatibility. - - It tries to unify the suffix of 2 lists element by element and if - it reaches the end of a list, it returns the remaining elements in - the other list if there are some. -*) let ise_exact ise x1 x2 = match ise x1 x2 with | None, out -> out -- cgit v1.2.3 From 9fa7f38b74ec26f880d9ec983a5a1c8699e0a612 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Apr 2015 16:35:15 +0200 Subject: Fixing #3383 (a "return" clause without an "in" clause is not enough for being able to interpret a "match" as a constr pattern). --- pretyping/patternops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 705e594af1..a766b1265e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function | Some p, Some (_,_,nal) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | _ -> PMeta None + | (None | Some (GHole _)), None -> PMeta None + | Some p, None -> + user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; -- cgit v1.2.3 From a45bd5981092cceefc4d4d30f9be327bb69c22d8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 21 Apr 2015 16:36:31 +0200 Subject: Fixing #4198 (looking for subterms also in the return clause of match). This is actually not so perfect because of the lambdas in the return clause which we would not like to look in. --- pretyping/constr_matching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 161cffa865..e281807131 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, c1) :: subargs env lc in + let sub = (env, hd) :: (env, c1) :: subargs env lc in let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> -- cgit v1.2.3 From db294322a9ae8954d5325ad0f02e37bf0db70548 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 22 Apr 2015 18:50:05 +0200 Subject: Fixing non exhaustive pattern-matching. --- pretyping/patternops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a766b1265e..fb629d049f 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -395,7 +395,7 @@ let rec pat_of_raw metas vars = function | Some p, Some (_,_,nal) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (GHole _)), None -> PMeta None + | (None | Some (GHole _)), _ -> PMeta None | Some p, None -> user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in -- cgit v1.2.3 From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 22 Apr 2015 18:51:48 +0200 Subject: Tactical `progress` compares term up to potentially equalisable universes. Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.--- pretyping/evarutil.ml | 21 ++++++++++++++++++++- pretyping/evarutil.mli | 7 +++++++ pretyping/evd.ml | 3 --- pretyping/evd.mli | 4 ---- 4 files changed, 27 insertions(+), 8 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 201a16ebeb..2508f4ef3b 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -844,6 +844,25 @@ let subterm_source evk (loc,k) = (loc,Evar_kinds.SubEvar evk) -(** Term exploration up to isntantiation. *) +(** Term exploration up to instantiation. *) let kind_of_term_upto sigma t = Constr.kind (Reductionops.whd_evar sigma t) + +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +let eq_constr_univs_test sigma1 sigma2 t u = + (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) + let open Evd in + let b, c = + Universes.eq_constr_univs_infer_with + (fun t -> kind_of_term_upto sigma1 t) + (fun u -> kind_of_term_upto sigma2 u) + (universes sigma2) t u + in + if b then + try let _ = add_universe_constraints sigma2 c in true + with Univ.UniverseInconsistency _ | UniversesDiffer -> false + else false diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 49036798e6..f1d94b0a4f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -206,6 +206,13 @@ val flush_and_check_evars : evar_map -> constr -> constr value of [e] in [sigma] is (recursively) used. *) val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds diff --git a/pretyping/evd.ml b/pretyping/evd.ml index bf519fb7c0..f414d71dc1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in evdref := evd; b -let eq_constr_univs_test evd t u = - snd (eq_constr_univs evd t u) - (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index fe785a8314..eca6d60ad5 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -562,10 +562,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool (** Syntactic equality up to universes. *) -val eq_constr_univs_test : evar_map -> constr -> constr -> bool -(** Syntactic equality up to universes, throwing away the (consistent) constraints - in case of success. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -- cgit v1.2.3 From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Apr 2015 14:55:11 +0200 Subject: Remove almost all the uses of string concatenation when building error messages. Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. --- pretyping/unification.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 01e1154e58..c2281e13a5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context x (named_context env) then - error ("The variable "^(Id.to_string x)^" is already declared.") + errorlabstrm "Unification.make_abstraction_core" + (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else x in -- cgit v1.2.3