diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 23 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 1 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/unification.ml | 13 |
6 files changed, 31 insertions, 26 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 312bf4907f..a793e217d4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -298,7 +298,7 @@ let inductive_template env sigma tmloc ind = let ty = EConstr.of_constr ty in let ty' = substl subst ty in let sigma, e = - Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty' + Evarutil.new_evar env ~src:(hole_source n) sigma ty' in (sigma, e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 90af143a2d..cbf539c1e9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -567,8 +567,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with | Const (c, u), Const (c', u') when QConstant.equal env c c' -> - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - check_strict evd u u' + if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c + then + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' | Const _, Const _ -> UnifFailure (evd, NotSameHead) | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> if EInstance.is_empty u && EInstance.is_empty u' then Success evd @@ -1312,6 +1317,7 @@ let check_selected_occs env sigma c occ occs = raise (PretypeError (env,sigma,NoOccurrenceFound (c,None))) else () +(* Error local to the module *) exception TypingFailed of evar_map let set_of_evctx l = @@ -1342,12 +1348,6 @@ let thin_evars env sigma sign c = let c' = applyrec (env,0) c in (!sigma, c') -exception NotFoundInstance of exn -let () = CErrors.register_handler (function - | NotFoundInstance e -> - Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e) - | _ -> None) - let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in @@ -1490,9 +1490,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) - with e when CErrors.noncritical e -> - let e, info = Exninfo.capture e in - Exninfo.iraise (NotFoundInstance e, info) + with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ -> + user_err (Pp.str "Cannot find an instance.") else ((if debug_ho_unification () then let evi = Evd.find evd evk in @@ -1709,7 +1708,7 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let flags = default_flags env in - instantiate_evar evar_unify flags env evd' evk ty + instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *) | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index bdf3495479..f42c754ef5 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -523,6 +523,7 @@ let rec cases_pattern_of_glob_constr env na c = | Anonymous -> PatVar (Name id) end | GHole (_,_,_) -> PatVar na + | GRef (GlobRef.VarRef id,_) -> PatVar (Name id) | GRef (GlobRef.ConstructRef cstr,_) -> PatCstr (cstr,[],na) | GApp (c, l) -> begin match DAst.get c with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 3f68e3c78f..d06d6e01d1 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -525,7 +525,7 @@ let native_norm env sigma c ty = if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in let t0 = Unix.gettimeofday () in - Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd); + Nativelib.call_linker ~fatal:true ~prefix fn (Some upd); let t1 = Unix.gettimeofday () in if profile then stop_profiler profiler_pid; let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 06f7d92e62..b70ff20e32 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -139,7 +139,7 @@ let interp_known_universe_level_name evd qid = let qid = Nametab.locate_universe qid in Univ.Level.make qid -let interp_universe_level_name ~anon_rigidity evd qid = +let interp_universe_level_name evd qid = try evd, interp_known_universe_level_name evd qid with Not_found -> if Libnames.qualid_is_ident qid then (* Undeclared *) @@ -162,21 +162,15 @@ let interp_universe_level_name ~anon_rigidity evd qid = with UGraph.AlreadyDeclared -> evd in evd, level -let interp_universe_name ?loc evd l = - (* [univ_flexible_alg] can produce algebraic universes in terms *) - let anon_rigidity = univ_flexible in - let evd', l = interp_universe_level_name ~anon_rigidity evd l in - evd', l - -let interp_sort_name ?loc sigma = function +let interp_sort_name sigma = function | GSProp -> sigma, Univ.Level.sprop | GProp -> sigma, Univ.Level.prop | GSet -> sigma, Univ.Level.set - | GType l -> interp_universe_name ?loc sigma l + | GType l -> interp_universe_level_name sigma l let interp_sort_info ?loc evd l = List.fold_left (fun (evd, u) (l,n) -> - let evd', u' = interp_sort_name ?loc evd l in + let evd', u' = interp_sort_name evd l in let u' = Univ.Universe.make u' in let u' = match n with | 0 -> u' @@ -410,7 +404,7 @@ let interp_known_glob_level ?loc evd = function let interp_glob_level ?loc evd : glob_level -> _ = function | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd - | UNamed s -> interp_sort_name ?loc evd s + | UNamed s -> interp_sort_name evd s let interp_instance ?loc evd l = let evd, l' = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4d37c0ef60..982814fdfc 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -687,6 +687,17 @@ let eta_constructor_app env sigma f l1 term = | _ -> assert false) | _ -> assert false +(* If the terms are irrelevant, check that they have the same type. *) +let careful_infer_conv ~pb ~ts env sigma m n = + if Retyping.relevance_of_term env sigma m == Sorts.Irrelevant && + Retyping.relevance_of_term env sigma n == Sorts.Irrelevant + then + let tm = Retyping.get_type_of env sigma m in + let tn = Retyping.get_type_of env sigma n in + Option.bind (infer_conv ~pb:CONV ~ts env sigma tm tn) + (fun sigma -> infer_conv ~pb ~ts env sigma m n) + else infer_conv ~pb ~ts env sigma m n + let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn = let cM = Evarutil.whd_head_evar sigma curm @@ -1127,7 +1138,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e None else let ans = match flags.modulo_conv_on_closed_terms with - | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n + | Some convflags -> careful_infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in match ans with | Some sigma -> ans |