diff options
| author | Matthieu Sozeau | 2014-06-25 18:25:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-25 20:00:10 +0200 |
| commit | 6a778ef90ed626ead64e86e1eec5c506514bb00e (patch) | |
| tree | ae405974811f922e29dd9e449f3635f4c90b902b | |
| parent | 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 (diff) | |
In rewrite, wrong computation of the sort of the term to be rewritten in
generated an uncaught Not_found. This raises an anomaly now and the sort is
properly computed now (fixes a bug in CoLoR).
| -rw-r--r-- | tactics/rewrite.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index aa32e0e5c4..06d0a04cc2 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -53,7 +53,9 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - Nametab.global_of_path sp + try Nametab.global_of_path sp + with Not_found -> + anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting")) let find_reference dir s = let gr = lazy (try_find_global_reference dir s) in @@ -1527,7 +1529,6 @@ let cl_rewrite_clause_strat strat clause = tclTHEN (tactic_init_setoid ()) (fun gl -> let meta = Evarutil.new_meta() in - (* let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in *) try cl_rewrite_clause_tac strat (mkMeta meta) clause gl with RewriteFailure e -> tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl @@ -1888,7 +1889,7 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl = and car = nf car and rel = nf rel in check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in - let sort = sort_of_rel env evd' (pf_concl gl) in + let sort = sort_of_rel env evd' but in let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty; evd = Evd.diff cl'.evd (project gl) } in @@ -1942,6 +1943,7 @@ let general_s_rewrite_clause x = match x with | None -> general_s_rewrite None | Some id -> general_s_rewrite (Some id) + let general_s_rewrite_clause x y z w ~new_goals = newtactic_init_setoid () <*> Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals) |