diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 74 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 |
5 files changed, 51 insertions, 35 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 773fc15208..9c5fdcd1ce 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -477,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index 91c5774051..0e39215701 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -942,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the diff --git a/tactics/hints.ml b/tactics/hints.ml index 85ff028249..d28d4848c7 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -828,38 +828,48 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in - match EConstr.kind sigma cty with - | Prod _ -> - let sigma' = Evd.merge_context_set univ_flexible sigma ctx in - let ce = mk_clenv_from_env env sigma' None (c,cty) in - let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in - let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry" in - let nmiss = List.length (clenv_missing ce) in - let secvars = secvars_of_constr env sigma c in - let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in - let pat = match info.hint_pattern with - | Some p -> snd p | None -> pat - in - if Int.equal nmiss 0 then - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; - secvars; - code = with_uid (Res_pf(c,cty,ctx)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then - Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++ - str " will only be used by eauto"); - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) - end - | _ -> failwith "make_apply_entry" + match EConstr.kind sigma cty with + | Prod _ -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let c' = clenv_type (* ~reduce:false *) ce in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry" in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let secvars = secvars_of_constr env sigma c in + let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in + let pat = match info.hint_pattern with + | Some p -> snd p | None -> pat + in + if Int.equal nmiss 0 then + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; + secvars; + code = with_uid (Res_pf(c,cty,ctx)); }) + else begin + if not eapply then failwith "make_apply_entry"; + if verbose then begin + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + end; + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (ERes_pf(c,cty,ctx)); }) + end + | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose c is a constr diff --git a/tactics/inv.ml b/tactics/inv.ml index 755494c2d2..e467eacd97 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c430edf2e9..928530744a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -212,6 +212,9 @@ let clear_dependency_msg env sigma id err inglobal = str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_clear_dependency env sigma id err inglobal = user_err (clear_dependency_msg env sigma id err inglobal) @@ -228,6 +231,9 @@ let replacing_dependency_msg env sigma id err inglobal = str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_replacing_dependency env sigma id err inglobal = user_err (replacing_dependency_msg env sigma id err inglobal) |