From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- tactics/auto.ml | 694 +++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 483 insertions(+), 211 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 6a9ced3e..93ca89f4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* search_entry - Le constr correspond à la constante de tête de la conclusion. + Le constr correspond à la constante de tête de la conclusion. Une search_entry est un triplet comprenant : - - la liste des tactiques qui n'ont pas de pattern associé + - la liste des tactiques qui n'ont pas de pattern associé - la liste des tactiques qui ont un pattern - - un discrimination net borné (Btermdn.t) constitué de tous les + - un discrimination net borné (Btermdn.t) constitué de tous les patterns de la seconde liste de tactiques *) -type stored_data = pri_auto_tactic +type stored_data = int * pri_auto_tactic + (* First component is the index of insertion in the table, to keep most recent first semantics. *) + +let auto_tactic_ord code1 code2 = + match code1, code2 with + | Res_pf (c1, _), Res_pf (c2, _) + | ERes_pf (c1, _), ERes_pf (c2, _) + | Give_exact c1, Give_exact c2 + | Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> constr_ord c1 c2 + | Unfold_nth (EvalVarRef i1), Unfold_nth (EvalVarRef i2) -> Pervasives.compare i1 i2 + | Unfold_nth (EvalConstRef c1), Unfold_nth (EvalConstRef c2) -> + kn_ord (canonical_con c1) (canonical_con c2) + | Extern t1, Extern t2 -> Pervasives.compare t1 t2 + | _ -> Pervasives.compare code1 code2 module Bounded_net = Btermdn.Make(struct type t = stored_data - let compare = Pervasives.compare + let compare = pri_order_int end) type search_entry = stored_data list * stored_data list * Bounded_net.t let empty_se = ([],[],Bounded_net.create ()) -let eq_pri_auto_tactic x y = +let eq_pri_auto_tactic (_, x) (_, y) = if x.pri = y.pri && x.pat = y.pat then match x.code,y.code with | Res_pf(cstr,_),Res_pf(cstr1,_) -> @@ -118,15 +149,18 @@ let eq_pri_auto_tactic x y = let add_tac pat t st (l,l',dn) = match pat with | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn) - | Some pat -> if not (List.exists (eq_pri_auto_tactic t) l') then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn) + | Some pat -> + if not (List.exists (eq_pri_auto_tactic t) l') + then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn) -let rebuild_dn st (l,l',dn) = - (l, l', List.fold_left (fun dn t -> Bounded_net.add (Some st) dn (Option.get t.pat, t)) +let rebuild_dn st ((l,l',dn) : search_entry) = + (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) (Bounded_net.create ()) l') + let lookup_tacs (hdc,c) st (l,l',dn) = let l' = List.map snd (Bounded_net.lookup st dn c) in - let sl' = Sort.list pri_order l' in + let sl' = List.stable_sort pri_order_int l' in Sort.merge pri_order l sl' module Constr_map = Map.Make(RefOrdered) @@ -136,11 +170,138 @@ let is_transparent_gr (ids, csts) = function | ConstRef cst -> Cpred.mem cst csts | IndRef _ | ConstructRef _ -> false +let dummy_goal = Goal.V82.dummy_goal + +let translate_hint (go,p) = + let mk_clenv (c,t) = + let cl = mk_clenv_from dummy_goal (c,t) in {cl with env = empty_env } + in + let code = match p.code with + | Res_pf (c,t) -> Res_pf (c, mk_clenv (c,t)) + | ERes_pf (c,t) -> ERes_pf (c, mk_clenv (c,t)) + | Res_pf_THEN_trivial_fail (c,t) -> + Res_pf_THEN_trivial_fail (c, mk_clenv (c,t)) + | Give_exact c -> Give_exact c + | Unfold_nth e -> Unfold_nth e + | Extern t -> Extern t + in + (go,{ p with code = code }) + +let path_matches hp hints = + let rec aux hp hints k = + match hp, hints with + | PathAtom _, [] -> false + | PathAtom PathAny, (_ :: hints') -> k hints' + | PathAtom p, (h :: hints') -> + if p = h then k hints' else false + | PathStar hp', hints -> + k hints || aux hp' hints (fun hints' -> aux hp hints' k) + | PathSeq (hp, hp'), hints -> + aux hp hints (fun hints' -> aux hp' hints' k) + | PathOr (hp, hp'), hints -> + aux hp hints k || aux hp' hints k + | PathEmpty, _ -> false + | PathEpsilon, hints -> k hints + in aux hp hints (fun hints' -> true) + +let rec matches_epsilon = function + | PathAtom _ -> false + | PathStar _ -> true + | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p' + | PathOr (p, p') -> matches_epsilon p || matches_epsilon p' + | PathEmpty -> false + | PathEpsilon -> true + +let rec is_empty = function + | PathAtom _ -> false + | PathStar _ -> false + | PathSeq (p, p') -> is_empty p || is_empty p' + | PathOr (p, p') -> matches_epsilon p && matches_epsilon p' + | PathEmpty -> true + | PathEpsilon -> false + +let rec path_derivate hp hint = + let rec derivate_atoms hints hints' = + match hints, hints' with + | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs' + | [], [] -> PathEpsilon + | [], hints -> PathEmpty + | grs, [] -> PathAtom (PathHints grs) + | _, _ -> PathEmpty + in + match hp with + | PathAtom PathAny -> PathEpsilon + | PathAtom (PathHints grs) -> + (match grs, hint with + | h :: hints, PathAny -> PathEmpty + | hints, PathHints hints' -> derivate_atoms hints hints' + | _, _ -> assert false) + | PathStar p -> if path_matches p [hint] then hp else PathEpsilon + | PathSeq (hp, hp') -> + let hpder = path_derivate hp hint in + if matches_epsilon hp then + PathOr (PathSeq (hpder, hp'), path_derivate hp' hint) + else if is_empty hpder then PathEmpty + else PathSeq (hpder, hp') + | PathOr (hp, hp') -> + PathOr (path_derivate hp hint, path_derivate hp' hint) + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEmpty + +let rec normalize_path h = + match h with + | PathStar PathEpsilon -> PathEpsilon + | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty + | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p + | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p + | PathOr (p, q) -> + let p', q' = normalize_path p, normalize_path q in + if p = p' && q = q' then h + else normalize_path (PathOr (p', q')) + | PathSeq (p, q) -> + let p', q' = normalize_path p, normalize_path q in + if p = p' && q = q' then h + else normalize_path (PathSeq (p', q')) + | _ -> h + +let path_derivate hp hint = normalize_path (path_derivate hp hint) + +let rec pp_hints_path = function + | PathAtom (PathAny) -> str"." + | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs + | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" + | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p' + | PathOr (p, p') -> + str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")" + | PathEmpty -> str"Ø" + | PathEpsilon -> str"ε" + +let rec subst_hints_path subst hp = + match hp with + | PathAtom PathAny -> hp + | PathAtom (PathHints grs) -> + let gr' gr = fst (subst_global subst gr) in + let grs' = list_smartmap gr' grs in + if grs' == grs then hp else PathAtom (PathHints grs') + | PathStar p -> let p' = subst_hints_path subst p in + if p' == p then hp else PathStar p' + | PathSeq (p, q) -> + let p' = subst_hints_path subst p in + let q' = subst_hints_path subst q in + if p' == p && q' == q then hp else PathSeq (p', q') + | PathOr (p, q) -> + let p' = subst_hints_path subst p in + let q' = subst_hints_path subst q in + if p' == p && q' == q then hp else PathOr (p', q') + | _ -> hp + module Hint_db = struct type t = { hintdb_state : Names.transparent_state; + hintdb_cut : hints_path; hintdb_unfolds : Idset.t * Cset.t; + mutable hintdb_max_id : int; use_dn : bool; hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant @@ -148,8 +309,13 @@ module Hint_db = struct hintdb_nopat : (global_reference option * stored_data) list } + let next_hint_id t = + let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h + let empty st use_dn = { hintdb_state = st; + hintdb_cut = PathEmpty; hintdb_unfolds = (Idset.empty, Cset.empty); + hintdb_max_id = 0; use_dn = use_dn; hintdb_map = Constr_map.empty; hintdb_nopat = [] } @@ -157,47 +323,54 @@ module Hint_db = struct let find key db = try Constr_map.find key db.hintdb_map with Not_found -> empty_se - + let map_none db = - Sort.merge pri_order (List.map snd db.hintdb_nopat) [] - + List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) []) + let map_all k db = let (l,l',_) = find k db in - Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l' + List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l') let map_auto (k,c) db = let st = if db.use_dn then Some db.hintdb_state else None in let l' = lookup_tacs (k,c) st (find k db) in - Sort.merge pri_order (List.map snd db.hintdb_nopat) l' + List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) l') let is_exact = function | Give_exact _ -> true | _ -> false - let addkv gr v db = + let is_unfold = function + | Unfold_nth _ -> true + | _ -> false + + let addkv gr id v db = + let idv = id, v in let k = match gr with - | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr then None else Some gr + | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && + is_unfold v.code then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in let pat = if not db.use_dn && is_exact v.code then None else v.pat in match k with | None -> - if not (List.exists (fun (_, v') -> v = v') db.hintdb_nopat) then - { db with hintdb_nopat = (gr,v) :: db.hintdb_nopat } + if not (List.exists (fun (_, (_, v')) -> v = v') db.hintdb_nopat) then + { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } else db | Some gr -> let oval = find gr db in - { db with hintdb_map = Constr_map.add gr (add_tac pat v dnst oval) db.hintdb_map } + { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map } let rebuild_db st' db = let db' = { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map; hintdb_state = st'; hintdb_nopat = [] } in - List.fold_left (fun db (gr,v) -> addkv gr v db) db' db.hintdb_nopat + List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat - let add_one (k,v) db = + let add_one kv db = + let (k,v) = translate_hint kv in let st',db,rebuild = match v.code with | Unfold_nth egr -> @@ -211,13 +384,27 @@ module Hint_db = struct | _ -> db.hintdb_state, db, false in let db = if db.use_dn && rebuild then rebuild_db st' db else db - in addkv k v db + in addkv k (next_hint_id db) v db let add_list l db = List.fold_right add_one l db + let remove_sdl p sdl = list_smartfilter p sdl + let remove_he st p (sl1, sl2, dn as he) = + let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in + if sl1' == sl1 && sl2' == sl2 then he + else rebuild_dn st (sl1', sl2', dn) + + let remove_list grs db = + let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in + let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in + let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } + + let remove_one gr db = remove_list [gr] db + let iter f db = - f None (List.map snd db.hintdb_nopat); - Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map + f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat); + Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map let transparent_state db = db.hintdb_state @@ -225,6 +412,11 @@ module Hint_db = struct if db.use_dn then rebuild_db st db else { db with hintdb_state = st } + let add_cut path db = + { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) } + + let cut db = db.hintdb_cut + let unfolds db = db.hintdb_unfolds let use_dn db = db.use_dn @@ -255,6 +447,9 @@ let current_db_names () = (**************************************************************************) let auto_init : (unit -> unit) ref = ref (fun () -> ()) +let add_auto_init f = + let init = !auto_init in + auto_init := (fun () -> init (); f ()) let init () = searchtable := Hintdbmap.empty; !auto_init () let freeze () = !searchtable @@ -280,47 +475,51 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." -let dummy_goal = - {it = make_evar empty_named_context_val mkProp; - sigma = empty} +let name_of_constr c = try Some (global_of_constr c) with Not_found -> None -let make_exact_entry sigma pri (c,cty) = +let make_exact_entry sigma pri ?(name=PathAny) (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> let pat = snd (Pattern.pattern_of_constr sigma cty) in - let head = - try head_of_constr_reference (fst (head_constr cty)) - with _ -> failwith "make_exact_entry" + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_exact_entry" in - (Some head, - { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) + (Some hd, + { pri = (match pri with None -> 0 | Some p -> p); + pat = Some pat; + name = name; + code = Give_exact c }) -let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = +let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) = let cty = if hnf then hnf_constr env sigma cty else cty in match kind_of_term cty with | Prod _ -> let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in let pat = snd (Pattern.pattern_of_constr sigma c') in - let hd = (try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry") in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry" in let nmiss = List.length (clenv_missing ce) in if nmiss = 0 then (Some hd, { pri = (match pri with None -> nb_hyp cty | Some p -> p); pat = Some pat; - code = Res_pf(c,{ce with env=empty_env}) }) + name = name; + code = Res_pf(c,cty) }) else begin if not eapply then failwith "make_apply_entry"; if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, - { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); - pat = Some pat; - code = ERes_pf(c,{ce with env=empty_env}) }) + { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); + pat = Some pat; + name = name; + code = ERes_pf(c,cty) }) end | _ -> failwith "make_apply_entry" @@ -328,12 +527,12 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = c is a constr cty is the type of constr *) -let make_resolves env sigma flags pri c = - let cty = type_of env sigma c in +let make_resolves env sigma flags pri ?name c = + let cty = Retyping.get_type_of env sigma c in let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry sigma pri; make_apply_entry env sigma flags pri] + [make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name] in if ents = [] then errorlabstrm "Hint" @@ -345,7 +544,8 @@ let make_resolves env sigma flags pri c = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma (hname,_,htyp) = try - [make_apply_entry env sigma (true, true, false) None + [make_apply_entry env sigma (true, true, false) None + ~name:(PathHints [VarRef hname]) (mkVar hname, htyp)] with | Failure _ -> [] @@ -353,26 +553,30 @@ let make_resolve_hyp env sigma (hname,_,htyp) = (* REM : in most cases hintname = id *) let make_unfold eref = - (Some (global_of_evaluable_reference eref), + let g = global_of_evaluable_reference eref in + (Some g, { pri = 4; pat = None; + name = PathHints [g]; code = Unfold_nth eref }) let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in (hdconstr, - { pri=pri; + { pri = pri; pat = pat; - code= Extern tacast }) + name = PathAny; + code = Extern tacast }) -let make_trivial env sigma c = +let make_trivial env sigma ?(name=PathAny) c = let t = hnf_constr env sigma (type_of env sigma c) in let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; - pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce))); - code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) - + pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce))); + name = name; + code=Res_pf_THEN_trivial_fail(c,t) }) + open Vernacexpr (**************************************************************************) @@ -402,23 +606,39 @@ let add_transparency dbname grs b = st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') -type hint_action = | CreateDB of bool * transparent_state - | AddTransparency of evaluable_global_reference list * bool - | AddTactic of (global_reference option * pri_auto_tactic) list +let remove_hint dbname grs = + let db = get_db dbname in + let db' = Hint_db.remove_list grs db in + searchtable_add (dbname, db') + +type hint_action = + | CreateDB of bool * transparent_state + | AddTransparency of evaluable_global_reference list * bool + | AddHints of hint_entry list + | RemoveHints of global_reference list + | AddCut of hints_path + +let add_cut dbname path = + let db = get_db dbname in + let db' = Hint_db.add_cut path db in + searchtable_add (dbname, db') + +type hint_obj = bool * string * hint_action (* locality, name, action *) let cache_autohint (_,(local,name,hints)) = match hints with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) | AddTransparency (grs, b) -> add_transparency name grs b - | AddTactic hints -> add_hint name hints + | AddHints hints -> add_hint name hints + | RemoveHints grs -> remove_hint name grs + | AddCut path -> add_cut name path let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") let set_extern_subst_tactic f = forward_subst_tactic := f -let subst_autohint (subst,(local,name,hintlist as obj)) = - let trans_clenv clenv = Clenv.subst_clenv subst clenv in +let subst_autohint (subst,(local,name,hintlist as obj)) = let subst_key gr = let (lab'', elab') = subst_global subst gr in let gr' = @@ -428,90 +648,72 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = in let subst_hint (k,data as hint) = let k' = Option.smartmap subst_key k in - let data' = match data.code with - | Res_pf (c, clenv) -> - let c' = subst_mps subst c in - let clenv' = trans_clenv clenv in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if c==c' && clenv'==clenv && pat'==data.pat then data else - {data with - pat=pat'; - code=Res_pf (c', clenv')} - | ERes_pf (c, clenv) -> - let c' = subst_mps subst c in - let clenv' = trans_clenv clenv in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if c==c' && clenv'==clenv && pat'==data.pat then data else - {data with - pat=pat'; - code=ERes_pf (c', clenv')} + let pat' = Option.smartmap (subst_pattern subst) data.pat in + let code' = match data.code with + | Res_pf (c,t) -> + let c' = subst_mps subst c in + let t' = subst_mps subst t in + if c==c' && t'==t then data.code else Res_pf (c', t') + | ERes_pf (c,t) -> + let c' = subst_mps subst c in + let t' = subst_mps subst t in + if c==c' && t'==t then data.code else ERes_pf (c',t') | Give_exact c -> - let c' = subst_mps subst c in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if c==c' && pat'==data.pat then data else - {data with - pat=pat'; - code=(Give_exact c')} - | Res_pf_THEN_trivial_fail (c, clenv) -> - let c' = subst_mps subst c in - let clenv' = trans_clenv clenv in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if c==c' && clenv'==clenv && pat'==data.pat then data else - {data with - pat=pat'; - code=Res_pf_THEN_trivial_fail (c',clenv')} + let c' = subst_mps subst c in + if c==c' then data.code else Give_exact c' + | Res_pf_THEN_trivial_fail (c,t) -> + let c' = subst_mps subst c in + let t' = subst_mps subst t in + if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t') | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if ref==ref' && pat'==data.pat then data else - {data with - pat=pat'; - code=(Unfold_nth ref')} + if ref==ref' then data.code else Unfold_nth ref' | Extern tac -> let tac' = !forward_subst_tactic subst tac in - let pat' = Option.smartmap (subst_pattern subst) data.pat in - if tac==tac' && pat'==data.pat then data else - {data with - pat=pat'; - code=(Extern tac')} + if tac==tac' then data.code else Extern tac' in - if k' == k && data' == data then hint else - (k',data') + let data' = + if data.pat==pat' && data.code==code' then data + else { data with pat = pat'; code = code' } + in + if k' == k && data' == data then hint else (k',data') in match hintlist with | CreateDB _ -> obj | AddTransparency (grs, b) -> let grs' = list_smartmap (subst_evaluable_reference subst) grs in if grs==grs' then obj else (local, name, AddTransparency (grs', b)) - | AddTactic hintlist -> + | AddHints hintlist -> let hintlist' = list_smartmap subst_hint hintlist in if hintlist' == hintlist then obj else - (local,name,AddTactic hintlist') + (local,name,AddHints hintlist') + | RemoveHints grs -> + let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in + if grs==grs' then obj else (local, name, RemoveHints grs') + | AddCut path -> + let path' = subst_hints_path subst path in + if path' == path then obj else (local, name, AddCut path') let classify_autohint ((local,name,hintlist) as obj) = - if local or hintlist = (AddTactic []) then Dispose else Substitute obj + if local or hintlist = (AddHints []) then Dispose else Substitute obj -let discharge_autohint (_,(local,name,hintlist as obj)) = - if local then None else - match hintlist with - | CreateDB _ -> - (* We assume that the transparent state is either empty or full *) - Some obj - | AddTransparency _ | AddTactic _ -> - (* Needs the adequate code here to support Global Hints in sections *) - None - -let (inAutoHint,_) = +let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); subst_function = subst_autohint; - classify_function = classify_autohint } - + classify_function = classify_autohint; } let create_hint_db l n st b = Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st))) +let remove_hints local dbnames grs = + let dbnames = if dbnames = [] then ["core"] else dbnames in + List.iter + (fun dbname -> + Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs))) + dbnames + (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) @@ -520,16 +722,21 @@ let add_resolves env sigma clist local dbnames = (fun dbname -> Lib.add_anonymous_leaf (inAutoHint - (local,dbname, AddTactic - (List.flatten (List.map (fun (x, hnf, y) -> - make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist))))) + (local,dbname, AddHints + (List.flatten (List.map (fun (x, hnf, path, y) -> + make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist))))) dbnames - let add_unfolds l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, AddTactic (List.map make_unfold l)))) + (inAutoHint (local,dbname, AddHints (List.map make_unfold l)))) + dbnames + +let add_cuts l local dbnames = + List.iter + (fun dbname -> Lib.add_anonymous_leaf + (inAutoHint (local,dbname, AddCut l))) dbnames let add_transparency l b local dbnames = @@ -550,10 +757,10 @@ let add_extern pri pat tacast local dbname = (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.") | [] -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast]))) + (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast]))) | None -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast])) + (inAutoHint(local,dbname, AddHints [make_extern pri None tacast])) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames @@ -562,7 +769,8 @@ let add_trivials env sigma l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf ( - inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l)))) + inAutoHint(local,dbname, + AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l)))) dbnames let forward_intern_tac = @@ -571,8 +779,9 @@ let forward_intern_tac = let set_extern_intern_tac f = forward_intern_tac := f type hints_entry = - | HintsResolveEntry of (int option * bool * constr) list - | HintsImmediateEntry of constr list + | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list + | HintsImmediateEntry of (hints_path_atom * constr) list + | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsExternEntry of @@ -580,24 +789,69 @@ type hints_entry = | HintsDestructEntry of identifier * int * (bool,unit) location * (patvar list * constr_pattern) * glob_tactic_expr +let h = id_of_string "H" + +exception Found of constr * types + +let prepare_hint env (sigma,c) = + let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in + (* We re-abstract over uninstantiated evars. + It is actually a bit stupid to generalize over evars since the first + thing make_resolves will do is to re-instantiate the products *) + let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in + let vars = ref (collect_vars c) in + let subst = ref [] in + let rec find_next_evar c = match kind_of_term c with + | Evar (evk,args as ev) -> + (* We skip the test whether args is the identity or not *) + let t = Evarutil.nf_evar sigma (existential_type sigma ev) in + let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in + if free_rels t <> Intset.empty then + error "Hints with holes dependent on a bound variable not supported."; + if occur_existential t then + (* Not clever enough to construct dependency graph of evars *) + error "Not clever enough to deal with evars dependent in other evars."; + raise (Found (c,t)) + | _ -> iter_constr find_next_evar c in + let rec iter c = + try find_next_evar c; c + with Found (evar,t) -> + let id = next_ident_away_from h (fun id -> Idset.mem id !vars) in + vars := Idset.add id !vars; + subst := (evar,mkVar id)::!subst; + mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in + iter c + +let path_of_constr_expr c = + match c with + | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | _ -> PathAny + let interp_hints h = - let f = Constrintern.interp_constr Evd.empty (Global.env()) in + let f c = + let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in + let c = prepare_hint (Global.env()) (evd,c) in + Evarutil.check_evars (Global.env()) Evd.empty evd c; + c in let fr r = let gr = global_with_alias r in let r' = evaluable_of_global_reference (Global.env()) gr in Dumpglob.add_glob (loc_of_reference r) gr; r' in + let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in + let fi c = path_of_constr_expr c, f c in let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in match h with - | HintsResolve lhints -> HintsResolveEntry (List.map (on_pi3 f) lhints) - | HintsImmediate lhints -> HintsImmediateEntry (List.map f lhints) + | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) | HintsTransparency (lhints, b) -> HintsTransparencyEntry (List.map fr lhints, b) | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in - list_tabulate (fun i -> None, true, mkConstruct (ind,i+1)) + list_tabulate (fun i -> let c = (ind,i+1) in + None, true, PathHints [ConstructRef c], mkConstruct c) (nconstructors ind) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> @@ -609,11 +863,14 @@ let interp_hints h = HintsDestructEntry (na,pri,loc,pat,!forward_intern_tac l code) let add_hints local dbnames0 h = + if List.mem "nocore" dbnames0 then + error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in let env = Global.env() and sigma = Evd.empty in match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames + | HintsCutEntry lhints -> add_cuts lhints local dbnames | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames | HintsTransparencyEntry (lhints, b) -> add_transparency lhints b local dbnames @@ -639,8 +896,8 @@ let pr_autotactic = | Extern tac -> (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) -let pr_hint v = - (pr_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) +let pr_hint (id, v) = + (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ()) @@ -655,7 +912,7 @@ let pr_hint_list_for_head c = let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = map_succeed - (fun (name,db) -> (name,db,Hint_db.map_all c db)) + (fun (name,db) -> (name,db, List.map (fun v -> 0, v) (Hint_db.map_all c db))) dbs in if valid_dbs = [] then @@ -682,6 +939,7 @@ let pr_hint_term cl = else Hint_db.map_auto (hd, applist (hdc,args)) with Bound -> Hint_db.map_none in + let fn db = List.map (fun x -> 0, x) (fn db) in map_succeed (fun (name, db) -> (name, db, fn db)) dbs in if valid_dbs = [] then @@ -700,8 +958,12 @@ let print_hint_term cl = ppnl (pr_hint_term cl) (* print all hints that apply to the concl of the current goal *) let print_applicable_hint () = let pts = get_pftreestate () in - let gl = nth_goal_of_pftreestate 1 pts in - print_hint_term (pf_concl gl) + let glss = Proof.V82.subgoals pts in + match glss.Evd.it with + | [] -> Util.error "No focused goal." + | g::_ -> + let gl = { Evd.it = g; sigma = glss.Evd.sigma } in + print_hint_term (pf_concl gl) (* displays the whole hint database db *) let print_hint_db db = @@ -711,17 +973,18 @@ let print_hint_db db = else str"Non-discriminated database"))); msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids)); msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts)); + msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db))); Hint_db.iter (fun head hintlist -> match head with | Some head -> msg (hov 0 (str "For " ++ pr_global head ++ str " -> " ++ - pr_hint_list hintlist)) + pr_hint_list (List.map (fun x -> (0,x)) hintlist))) | None -> msg (hov 0 (str "For any goal -> " ++ - pr_hint_list hintlist))) + pr_hint_list (List.map (fun x -> (0, x)) hintlist)))) db let print_hint_db_by_name dbname = @@ -746,7 +1009,7 @@ let print_searchtable () = (* tactics with a trace mechanism for automatic search *) (**************************************************************************) -let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l +let priority l = List.filter (fun (_, hint) -> hint.pri = 0) l (* tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds oftener) *) @@ -755,10 +1018,18 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = true; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; + frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* Compat *) + modulo_betaiota = false; + modulo_eta = true; + allow_K_in_toplevel_higher_order_unification = false } (* Try unification with the precompiled clause, then use registered Apply *) @@ -769,12 +1040,12 @@ let h_clenv_refine ev c clenv = let unify_resolve_nodelta (c,clenv) gl = let clenv' = connect_clenv gl clenv in - let clenv'' = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in + let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in h_clenv_refine false c clenv'' gl let unify_resolve flags (c,clenv) gl = let clenv' = connect_clenv gl clenv in - let clenv'' = clenv_unique_resolver false ~flags clenv' gl in + let clenv'' = clenv_unique_resolver ~flags clenv' gl in h_clenv_refine false c clenv'' gl let unify_resolve_gen = function @@ -783,40 +1054,44 @@ let unify_resolve_gen = function (* Util *) -let expand_constructor_hints lems = - list_map_append (fun lem -> +let expand_constructor_hints env lems = + list_map_append (fun (sigma,lem) -> match kind_of_term lem with | Ind ind -> list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind) | _ -> - [lem]) lems + [prepare_hint env (sigma,lem)]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) let add_hint_lemmas eapply lems hint_db gl = - let lems = expand_constructor_hints lems in + let lems = expand_constructor_hints (pf_env gl) lems in let hintlist' = list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in Hint_db.add_list hintlist' hint_db -let make_local_hint_db eapply lems gl = +let make_local_hint_db ?ts eapply lems gl = let sign = pf_hyps gl in + let ts = match ts with + | None -> Hint_db.transparent_state (searchtable_map "core") + | Some ts -> ts + in let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in add_hint_lemmas eapply lems - (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false)) gl + (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl (* Serait-ce possible de compiler d'abord la tactique puis de faire la - substitution sans passer par bdize dont l'objectif est de préparer un + substitution sans passer par bdize dont l'objectif est de préparer un terme pour l'affichage ? (HH) *) -(* Si on enlève le dernier argument (gl) conclPattern est calculé une +(* Si on enlève le dernier argument (gl) conclPattern est calculé une fois pour toutes : en particulier si Pattern.somatch produit une UserError -Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même -si après Intros la conclusion matche le pattern. +Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même +si après Intros la conclusion matche le pattern. *) -(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) +(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) let forward_interp_tactic = ref (fun _ -> failwith "interp_tactic is not installed for auto") @@ -837,8 +1112,8 @@ let conclPattern concl pat tac gl = (**************************************************************************) (* local_db is a Hint database containing the hypotheses of current goal *) -(* Papageno : cette fonction a été pas mal simplifiée depuis que la base - de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) +(* Papageno : cette fonction a été pas mal simplifiée depuis que la base + de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = {auto_unif_flags with @@ -864,7 +1139,7 @@ let rec trivial_fail_db mod_delta db_list local_db gl = in tclFIRST (assumption::intro_tac:: - (List.map tclCOMPLETE + (List.map (fun tac -> tclCOMPLETE tac) (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl and my_find_search_nodelta db_list local_db hdc concl = @@ -876,7 +1151,7 @@ and my_find_search mod_delta = else my_find_search_nodelta and my_find_search_delta db_list local_db hdc concl = - let flags = {auto_unif_flags with use_metas_eagerly = true} in + let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in let f = hintmap_of hdc concl in if occur_existential concl then list_map_append @@ -906,20 +1181,23 @@ and my_find_search_delta db_list local_db hdc concl = in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) -and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) = - match t with - | Res_pf (term,cl) -> unify_resolve_gen flags (term,cl) - | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_check c - | Res_pf_THEN_trivial_fail (term,cl) -> +and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) = + let tactic = + match t with + | Res_pf (c,cl) -> unify_resolve_gen flags (c,cl) + | ERes_pf _ -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_check c + | Res_pf_THEN_trivial_fail (c,cl) -> tclTHEN - (unify_resolve_gen flags (term,cl)) + (unify_resolve_gen flags (c,cl)) (trivial_fail_db (flags <> None) db_list local_db) - | Unfold_nth c -> (fun gl -> - if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl - else tclFAIL 0 (str"Unbound reference") gl) - | Extern tacast -> conclPattern concl p tacast + | Unfold_nth c -> + (fun gl -> + if exists_evaluable_reference (pf_env gl) c then + tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl + else tclFAIL 0 (str"Unbound reference") gl) + | Extern tacast -> conclPattern concl p tacast + in tactic and trivial_resolve mod_delta db_list local_db cl = try @@ -933,21 +1211,25 @@ and trivial_resolve mod_delta db_list local_db cl = (my_find_search mod_delta db_list local_db head cl)) with Not_found -> [] -let trivial lems dbnames gl = - let db_list = - List.map - (fun x -> - try - searchtable_map x - with Not_found -> - error_no_such_hint_database x) - ("core"::dbnames) +(** The use of the "core" database can be de-activated by passing + "nocore" amongst the databases. *) + +let make_db_list dbnames = + let use_core = not (List.mem "nocore" dbnames) in + let dbnames = list_remove "nocore" dbnames in + let dbnames = if use_core then "core"::dbnames else dbnames in + let lookup db = + try searchtable_map db with Not_found -> error_no_such_hint_database db in + List.map lookup dbnames + +let trivial lems dbnames gl = + let db_list = make_db_list dbnames in tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl let full_trivial lems gl = let dbnames = Hintdbmap.dom !searchtable in - let dbnames = list_subtract dbnames ["v62"] in + let dbnames = list_remove "v62" dbnames in let db_list = List.map (fun x -> searchtable_map x) dbnames in tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl @@ -955,10 +1237,8 @@ let gen_trivial lems = function | None -> full_trivial lems | Some l -> trivial lems l -let inj_open c = (Evd.empty,c) - let h_trivial lems l = - Refiner.abstract_tactic (TacTrivial (lems,l)) + Refiner.abstract_tactic (TacTrivial (List.map snd lems,l)) (gen_trivial lems l) (**************************************************************************) @@ -1051,15 +1331,7 @@ let search = search_gen 0 let default_search_depth = ref 5 let delta_auto mod_delta n lems dbnames gl = - let db_list = - List.map - (fun x -> - try - searchtable_map x - with Not_found -> - error_no_such_hint_database x) - ("core"::dbnames) - in + let db_list = make_db_list dbnames in tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl let auto = delta_auto false @@ -1070,7 +1342,7 @@ let default_auto = auto !default_search_depth [] [] let delta_full_auto mod_delta n lems gl = let dbnames = Hintdbmap.dom !searchtable in - let dbnames = list_subtract dbnames ["v62"] in + let dbnames = list_remove "v62" dbnames in let db_list = List.map (fun x -> searchtable_map x) dbnames in tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl @@ -1088,7 +1360,7 @@ let gen_auto n lems dbnames = let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto n lems l = - Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) + Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map snd lems,l)) (gen_auto n lems l) (**************************************************************************) @@ -1117,7 +1389,7 @@ let dauto (n,p) lems = let default_dauto = dauto (None,None) [] let h_dauto (n,p) lems = - Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,lems)) + Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems)) (dauto (n,p) lems) (***************************************) -- cgit v1.2.3 From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- .gitignore | 3 + CHANGES | 56 +- COPYRIGHT | 2 +- CREDITS | 10 +- INSTALL | 6 +- Makefile | 2 +- Makefile.build | 14 +- Makefile.common | 17 +- Makefile.doc | 44 +- README | 6 +- TODO | 53 - checker/mod_checking.ml | 74 +- checker/subtyping.ml | 58 +- configure | 29 +- dev/base_include | 6 +- dev/printers.mllib | 2 +- dev/top_printers.ml | 4 + doc/common/macros.tex | 1 + doc/common/styles/html/coqremote/cover.html | 9 +- doc/common/styles/html/coqremote/footer.html | 45 + doc/common/styles/html/coqremote/header.html | 49 + doc/common/styles/html/simple/cover.html | 10 +- doc/common/styles/html/simple/footer.html | 2 + doc/common/styles/html/simple/header.html | 13 + doc/common/title.tex | 2 +- doc/faq/FAQ.tex | 6 +- doc/refman/Cases.tex | 2 +- doc/refman/RefMan-cic.tex | 77 +- doc/refman/RefMan-coi.tex | 4 +- doc/refman/RefMan-com.tex | 176 +- doc/refman/RefMan-ext.tex | 41 +- doc/refman/RefMan-gal.tex | 4 +- doc/refman/RefMan-ltac.tex | 3 +- doc/refman/RefMan-oth.tex | 138 +- doc/refman/RefMan-pro.tex | 79 +- doc/refman/RefMan-sch.tex | 418 ++ doc/refman/RefMan-syn.tex | 2 +- doc/refman/RefMan-tac.tex | 6168 ++++++++++++------------ doc/refman/RefMan-tacex.tex | 584 --- doc/refman/RefMan-uti.tex | 52 +- doc/refman/Reference-Manual.tex | 7 +- doc/refman/coqdoc.tex | 12 +- doc/stdlib/hidden-files | 0 doc/stdlib/index-list.html.template | 36 +- doc/stdlib/index-trailer.html | 2 - doc/stdlib/make-library-index | 34 +- ide/command_windows.ml | 24 +- ide/command_windows.mli | 2 + ide/coq.ml | 120 +- ide/coq.mli | 14 +- ide/coq_commands.ml | 1 - ide/coq_lex.mll | 28 +- ide/coqide-gtk2rc | 10 - ide/coqide.ml | 231 +- ide/coqide.mli | 3 - ide/coqide_main.ml4 | 24 +- ide/coqide_ui.ml | 28 +- ide/ideproof.ml | 16 +- ide/ideutils.ml | 99 +- ide/ideutils.mli | 13 + ide/minilib.ml | 47 +- ide/preferences.ml | 210 +- ide/preferences.mli | 21 +- ide/tags.ml | 33 +- ide/tags.mli | 50 + ide/utils/configwin.ml | 4 +- ide/utils/configwin_ihm.ml | 6 +- interp/constrextern.ml | 50 +- interp/constrextern.mli | 1 + interp/constrintern.ml | 70 +- interp/constrintern.mli | 3 + interp/genarg.ml | 42 +- interp/genarg.mli | 6 +- interp/notation.ml | 5 + interp/notation.mli | 2 + interp/topconstr.ml | 15 +- interp/topconstr.mli | 4 + kernel/declarations.mli | 4 + kernel/mod_typing.ml | 82 +- kernel/safe_typing.ml | 56 +- kernel/safe_typing.mli | 2 +- kernel/subtyping.ml | 74 +- kernel/term.ml | 1 + kernel/term.mli | 6 +- kernel/univ.ml | 111 +- kernel/univ.mli | 4 + lib/envars.ml | 6 +- lib/explore.ml | 18 +- lib/explore.mli | 2 +- lib/pp.ml4 | 19 +- lib/pp.mli | 3 + lib/util.ml | 25 +- lib/util.mli | 6 + lib/xml_parser.mli | 2 +- library/assumptions.ml | 18 +- library/declare.ml | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/goptions.ml | 1 + library/impargs.ml | 13 +- library/lib.ml | 111 +- library/lib.mli | 43 +- man/coqc.1 | 12 + man/coqtop.1 | 8 +- myocamlbuild.ml | 9 + parsing/argextend.ml4 | 74 +- parsing/egrammar.ml | 41 +- parsing/egrammar.mli | 2 + parsing/extrawit.ml | 12 +- parsing/g_constr.ml4 | 24 +- parsing/g_proofs.ml4 | 21 +- parsing/g_tactic.ml4 | 27 +- parsing/g_vernac.ml4 | 4 +- parsing/ppconstr.ml | 72 +- parsing/ppconstr.mli | 6 +- parsing/pptactic.ml | 30 +- parsing/ppvernac.ml | 76 +- parsing/printer.ml | 37 +- parsing/printer.mli | 3 +- parsing/q_coqast.ml4 | 15 +- parsing/tacextend.ml4 | 61 +- plugins/decl_mode/g_decl_mode.ml4 | 5 +- plugins/dp/Dp.v | 118 - plugins/dp/TODO | 24 - plugins/dp/dp.ml | 1133 ----- plugins/dp/dp.mli | 20 - plugins/dp/dp_plugin.mllib | 5 - plugins/dp/dp_why.ml | 185 - plugins/dp/dp_why.mli | 17 - plugins/dp/dp_zenon.mli | 7 - plugins/dp/dp_zenon.mll | 189 - plugins/dp/fol.mli | 58 - plugins/dp/g_dp.ml4 | 77 - plugins/dp/test2.v | 80 - plugins/dp/tests.v | 300 -- plugins/dp/vo.itarget | 1 - plugins/dp/zenon.v | 92 - plugins/extraction/extract_env.ml | 11 +- plugins/extraction/modutil.ml | 11 +- plugins/firstorder/g_ground.ml4 | 2 - plugins/funind/functional_principles_proofs.ml | 3 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 55 +- plugins/funind/recdef.ml | 42 +- plugins/micromega/coq_micromega.ml | 19 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/pluginsbyte.itarget | 1 - plugins/pluginsdyn.itarget | 1 - plugins/pluginsopt.itarget | 1 - plugins/pluginsvo.itarget | 3 +- plugins/rtauto/proof_search.ml | 4 +- plugins/rtauto/proof_search.mli | 2 +- plugins/subtac/eterm.ml | 17 +- plugins/subtac/g_subtac.ml4 | 4 +- plugins/subtac/subtac.ml | 4 +- plugins/subtac/subtac_cases.ml | 2 +- plugins/subtac/subtac_classes.ml | 9 +- plugins/subtac/subtac_coercion.ml | 107 +- plugins/subtac/subtac_command.ml | 2 +- plugins/subtac/subtac_obligations.ml | 25 +- plugins/subtac/subtac_pretyping.ml | 4 +- plugins/subtac/subtac_pretyping_F.ml | 33 +- plugins/subtac/subtac_utils.ml | 11 +- plugins/subtac/subtac_utils.mli | 1 + plugins/xml/dumptree.ml4 | 4 +- pretyping/cases.ml | 5 +- pretyping/coercion.ml | 2 +- pretyping/detyping.ml | 8 +- pretyping/evarconv.ml | 119 +- pretyping/evarutil.ml | 1503 +++--- pretyping/evarutil.mli | 6 +- pretyping/evd.ml | 10 +- pretyping/evd.mli | 2 + pretyping/inductiveops.ml | 19 +- pretyping/namegen.ml | 47 +- pretyping/namegen.mli | 5 +- pretyping/pretyping.ml | 9 +- pretyping/pretyping.mli | 3 +- pretyping/tacred.ml | 12 +- pretyping/typeclasses.ml | 34 +- pretyping/typeclasses.mli | 12 +- pretyping/unification.ml | 2 +- pretyping/vnorm.ml | 9 +- proofs/clenv.ml | 4 +- proofs/evar_refiner.ml | 2 +- proofs/goal.ml | 6 +- proofs/goal.mli | 4 +- proofs/logic.ml | 8 +- proofs/pfedit.ml | 14 +- proofs/pfedit.mli | 22 +- proofs/proof.ml | 134 +- proofs/proof.mli | 14 +- proofs/proof_global.ml | 72 +- proofs/proof_global.mli | 6 - proofs/proofview.ml | 11 + proofs/proofview.mli | 5 + proofs/refiner.ml | 4 - proofs/refiner.mli | 1 - proofs/tacexpr.ml | 11 +- proofs/tacmach.ml | 8 - proofs/tacmach.mli | 3 - proofs/tactic_debug.ml | 103 +- proofs/tactic_debug.mli | 7 + scripts/coqc.ml | 23 +- tactics/auto.ml | 417 +- tactics/auto.mli | 54 +- tactics/class_tactics.ml4 | 37 +- tactics/dhyp.ml | 359 -- tactics/dhyp.mli | 28 - tactics/eauto.ml4 | 146 +- tactics/eauto.mli | 4 +- tactics/extraargs.ml4 | 35 +- tactics/extraargs.mli | 2 + tactics/extratactics.ml4 | 18 +- tactics/refine.ml | 2 +- tactics/rewrite.ml4 | 22 +- tactics/tacinterp.ml | 605 ++- tactics/tacinterp.mli | 14 +- tactics/tacticals.ml | 1 - tactics/tacticals.mli | 1 - tactics/tactics.ml | 10 +- tactics/tactics.mllib | 1 - test-suite/bugs/closed/shouldsucceed/2603.v | 21 +- test-suite/bugs/closed/shouldsucceed/2732.v | 19 + test-suite/bugs/closed/shouldsucceed/2733.v | 26 + test-suite/complexity/autodecomp.v | 11 - test-suite/output/Arguments.out | 8 + test-suite/output/Arguments.v | 12 + test-suite/output/Notations2.out | 6 + test-suite/output/Notations2.v | 15 + test-suite/output/PrintInfos.out | 9 +- test-suite/success/Cases.v | 71 +- test-suite/success/CasesDep.v | 22 +- test-suite/success/Hints.v | 5 - test-suite/success/Mod_params.v | 84 +- test-suite/success/Notations.v | 14 +- test-suite/success/RecTutorial.v | 69 +- test-suite/success/Reset.v | 7 - test-suite/success/apply.v | 17 +- test-suite/success/coercions.v | 42 + test-suite/success/dependentind.v | 31 + test-suite/success/evars.v | 70 + test-suite/success/hyps_inclusion.v | 8 +- test-suite/success/telescope_canonical.v | 70 +- theories/Arith/Div2.v | 26 +- theories/Init/Logic.v | 4 +- theories/Init/Prelude.v | 1 - theories/Init/Specif.v | 2 +- theories/Lists/intro.tex | 2 +- theories/Logic/ChoiceFacts.v | 16 +- theories/MSets/MSetAVL.v | 1377 +----- theories/MSets/MSetGenTree.v | 1145 +++++ theories/MSets/MSetRBT.v | 1931 ++++++++ theories/MSets/vo.itarget | 2 + theories/Program/Equality.v | 26 +- theories/Unicode/Utf8_core.v | 4 +- theories/Vectors/Fin.v | 10 +- theories/Vectors/VectorDef.v | 23 +- theories/Vectors/VectorSpec.v | 6 + theories/Wellfounded/Lexicographic_Product.v | 14 +- theories/ZArith/Int.v | 128 +- theories/ZArith/ZOdiv.v | 88 + theories/ZArith/ZOdiv_def.v | 15 + theories/ZArith/Zeven.v | 6 +- theories/ZArith/vo.itarget | 2 + tools/coq_makefile.ml | 26 +- tools/coqdoc/cpretty.mll | 20 +- tools/coqdoc/index.ml | 6 +- tools/coqdoc/output.ml | 8 +- tools/win32hack.mllib | 1 + tools/win32hack_filename.ml | 4 + toplevel/backtrack.ml | 225 + toplevel/backtrack.mli | 93 + toplevel/class.ml | 2 +- toplevel/classes.ml | 9 +- toplevel/command.ml | 36 +- toplevel/coqtop.ml | 11 +- toplevel/himsg.ml | 16 +- toplevel/ide_intf.ml | 120 +- toplevel/ide_intf.mli | 26 + toplevel/ide_slave.ml | 436 +- toplevel/interface.mli | 47 +- toplevel/metasyntax.ml | 12 + toplevel/metasyntax.mli | 2 + toplevel/mltop.ml4 | 23 +- toplevel/mltop.mli | 10 + toplevel/record.ml | 6 +- toplevel/search.mli | 2 + toplevel/toplevel.ml | 3 - toplevel/toplevel.mllib | 1 + toplevel/vernac.ml | 65 +- toplevel/vernac.mli | 9 +- toplevel/vernacentries.ml | 198 +- toplevel/vernacentries.mli | 31 +- toplevel/vernacexpr.ml | 28 +- 295 files changed, 12968 insertions(+), 11382 deletions(-) delete mode 100644 TODO create mode 100644 doc/common/styles/html/coqremote/footer.html create mode 100644 doc/common/styles/html/coqremote/header.html create mode 100644 doc/common/styles/html/simple/footer.html create mode 100644 doc/common/styles/html/simple/header.html create mode 100644 doc/refman/RefMan-sch.tex create mode 100644 doc/stdlib/hidden-files delete mode 100644 doc/stdlib/index-trailer.html create mode 100644 ide/tags.mli delete mode 100644 plugins/dp/Dp.v delete mode 100644 plugins/dp/TODO delete mode 100644 plugins/dp/dp.ml delete mode 100644 plugins/dp/dp.mli delete mode 100644 plugins/dp/dp_plugin.mllib delete mode 100644 plugins/dp/dp_why.ml delete mode 100644 plugins/dp/dp_why.mli delete mode 100644 plugins/dp/dp_zenon.mli delete mode 100644 plugins/dp/dp_zenon.mll delete mode 100644 plugins/dp/fol.mli delete mode 100644 plugins/dp/g_dp.ml4 delete mode 100644 plugins/dp/test2.v delete mode 100644 plugins/dp/tests.v delete mode 100644 plugins/dp/vo.itarget delete mode 100644 plugins/dp/zenon.v delete mode 100644 tactics/dhyp.ml delete mode 100644 tactics/dhyp.mli create mode 100644 test-suite/bugs/closed/shouldsucceed/2732.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2733.v delete mode 100644 test-suite/complexity/autodecomp.v delete mode 100644 test-suite/success/Reset.v create mode 100644 theories/MSets/MSetGenTree.v create mode 100644 theories/MSets/MSetRBT.v create mode 100644 theories/ZArith/ZOdiv.v create mode 100644 theories/ZArith/ZOdiv_def.v create mode 100644 tools/win32hack.mllib create mode 100644 tools/win32hack_filename.ml create mode 100644 toplevel/backtrack.ml create mode 100644 toplevel/backtrack.mli (limited to 'tactics/auto.ml') diff --git a/.gitignore b/.gitignore index 7fcd2580..32a40af6 100644 --- a/.gitignore +++ b/.gitignore @@ -79,6 +79,9 @@ doc/stdlib/Library.out doc/stdlib/Library.pdf doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex +doc/stdlib/FullLibrary.pdf +doc/stdlib/FullLibrary.ps +doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/html/ doc/stdlib/index-body.html doc/stdlib/index-list.html diff --git a/CHANGES b/CHANGES index 74aefe49..c245fb25 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,54 @@ -Changes from V8.3 to V8.4 -========================= +Changes from V8.4beta to V8.4 +============================= + +Vernacular commands + +- Undo and UndoTo are now handling the proof states. They may + perform some extra steps of backtrack to avoid states where + the proof state is unavailable (typically a closed proof). +- The commands Suspend and Resume have been removed. +- A basic Show Script has been reintroduced (no indentation). +- New command "Set Parsing Explicit" for deactivating parsing (and printing) + of implicit arguments (useful for teaching). +- New command "Grab Existential Variables" to transform the unresolved evars at + the end of a proof into goals. + +Tactics + +- Still no general "info" tactical, but new specific tactics + info_auto, info_eauto, info_trivial which provides information + on the proofs found by auto/eauto/trivial. Display of these + details could also be activated by Set Info Auto/Eauto/Trivial. +- Details on everything tried by auto/eauto/trivial during + a proof search could be obtained by "debug auto", "debug eauto", + "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". +- New command "r string" that interprets "idtac string" as a breakpoint + and jumps to its next use in Ltac debugger. +- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, + harvey, zenon, gwhy) have been removed, since Why2 has not been + maintained for the last few years. The Why3 plugin should be a suitable + replacement in most cases. + +Libraries + +- MSetRBT : a new implementation of MSets via Red-Black trees (initial + contribution by Andrew Appel). +- MSetAVL : for maximal sharing with the new MSetRBT, the argument order + of Node has changed (this should be transparent to regular MSets users). + +Module System + +- The names of modules (and module types) are now in a fully separated + namespace from ordinary definitions : "Definition E:=0. Module E. End E." + is now accepted. + +CoqIDE + +- Coqide now supports the Restart command, and Undo (with a warning). + Better support for Abort. + +Changes from V8.3 to V8.4beta +============================= Logic @@ -69,6 +118,8 @@ Tactics - When applying destruct or inversion on a fixpoint hiding an inductive type, recursive calls to the fixpoint now remain folded by default (rare source of incompatibility generally solvable by adding a call to simpl). +- The behavior of the simpl tactic can be tuned using the new "Arguments" + vernacular. Vernacular commands @@ -90,6 +141,7 @@ Vernacular commands to avoid conversion at Qed time to go into a very long computation. - New command "Show Goal ident" to display the statement of a goal, even a closed one (available from Proof General). +- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope". Module System diff --git a/COPYRIGHT b/COPYRIGHT index 8d81d8c4..3aa6aae9 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,6 +1,6 @@ The Coq proof assistant -Copyright 1999-2010 The Coq development team, INRIA, CNRS, University +Copyright 1999-2012 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by diff --git a/CREDITS b/CREDITS index 53bd9e93..543cb3f3 100644 --- a/CREDITS +++ b/CREDITS @@ -106,6 +106,7 @@ The following people have contributed to the development of different versions of the Coq Proof assistant during the indicated time: Bruno Barras (INRIA, 1995-now) + Pierre Boutillier (INRIA-PPS, 2010-now) Jacek Chrzaszcz (LRI, 1998-2003) Thierry Coquand (INRIA, 1985-1989) Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now) @@ -118,10 +119,12 @@ of the Coq Proof assistant during the indicated time: Amy Felty (INRIA, 1993) Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now) Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998) + Stéphane Glondu (INRIA-PPS, 2007-now) Benjamin Grégoire (INRIA, 2003-now) Hugo Herbelin (INRIA, 1996-now) Gérard Huet (INRIA, 1985-1997) - Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now) + Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now) + Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) @@ -132,9 +135,11 @@ of the Coq Proof assistant during the indicated time: Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now) Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) - Patrick Loiseleur (Paris Sud, 1997-1999) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-now) + Pierre-Marie Pédrot (INRIA-PPS, 2011-now) + Matthias Puech (INRIA-Bologna, 2008-now) + Yann Régis-Gianas (INRIA-PPS, 2009-now) Clément Renard (INRIA, 2001-2004) Claudio Sacerdoti Coen (INRIA, 2004-2005) Amokrane Saïbi (INRIA, 1993-1998) @@ -142,6 +147,7 @@ of the Coq Proof assistant during the indicated time: Élie Soubiran (INRIA, 2007-now) Matthieu Sozeau (INRIA, 2005-now) Arnaud Spiwack (INRIA, 2006-now) + Enrico Tassi (INRIA, 2011-now) Benjamin Werner (INRIA, 1989-1994) *************************************************************************** diff --git a/INSTALL b/INSTALL index e88dc319..5ee00613 100644 --- a/INSTALL +++ b/INSTALL @@ -39,9 +39,9 @@ WHAT DO YOU NEED ? urpmi coq - Should you need or prefer to compile Coq V8.2 yourself, you need: + Should you need or prefer to compile Coq V8.4 yourself, you need: - - Objective Caml version 3.10.0 or later + - Objective Caml version 3.11.2 or later (available at http://caml.inria.fr/) - Camlp5 (version <= 4.08, or 5.* transitional) @@ -87,7 +87,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.10.0 (or later) +1- Check that you have the Objective Caml compiler version 3.11.2 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. diff --git a/Makefile b/Makefile index 876ac583..0ff72856 100644 --- a/Makefile +++ b/Makefile @@ -191,6 +191,7 @@ docclean: rm -f doc/common/version.tex rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex + rm -f doc/refman/styles.hva doc/refman/cover.html archclean: clean-ide optclean voclean rm -rf _build myocamlbuild_config.ml @@ -221,7 +222,6 @@ cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli distclean: clean cleanconfig - $(MAKE) -C test-suite distclean voclean: rm -f states/*.coq diff --git a/Makefile.build b/Makefile.build index 59ee457c..41dfabbf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -318,7 +318,7 @@ $(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) $(STRIP) $@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) - $(SHOW)'OCAMLOPT -o $@' + $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\ str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) @@ -446,7 +446,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # 3) plugins ########################################################################### -.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction +.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction .PHONY: field fourier funind cc subtac rtauto pluginsopt plugins: $(PLUGINSVO) @@ -455,7 +455,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) ring: $(RINGVO) $(RINGCMA) setoid_ring: $(NEWRINGVO) $(NEWRINGCMA) nsatz: $(NSATZVO) $(NSATZCMA) -dp: $(DPCMA) xml: $(XMLVO) $(XMLCMA) extraction: $(EXTRACTIONCMA) field: $(FIELDVO) $(FIELDCMA) @@ -623,7 +622,7 @@ INSTALLCMI = $(sort \ install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib @@ -632,7 +631,7 @@ install-library: $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) + $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install # it with libraries @@ -643,11 +642,14 @@ endif install-library-light: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) +endif install-coq-info: install-coq-manpages install-emacs install-latex diff --git a/Makefile.common b/Makefile.common index b560bae5..3740b52e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -79,7 +79,7 @@ SRCDIRS:=\ pretyping interp toplevel/utils toplevel parsing \ ide/utils ide \ $(addprefix plugins/, \ - omega romega micromega quote ring dp \ + omega romega micromega quote ring \ setoid_ring xml extraction fourier \ cc funind firstorder field subtac \ rtauto nsatz syntax decl_mode) @@ -125,14 +125,15 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex \ + RefMan-decl.v.tex RefMan-sch.v.tex \ + RefMan-pro.v.tex \ Cases.v.tex Coercion.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Helm.tex Classes.v.tex ) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \ + RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ $(REFMANCOQTEXFILES) \ @@ -176,7 +177,6 @@ QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/ring/ring_plugin.cma NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -DPCMA:=plugins/dp/dp_plugin.cma FIELDCMA:=plugins/field/field_plugin.cma XMLCMA:=plugins/xml/xml_plugin.cma FOURIERCMA:=plugins/fourier/fourier_plugin.cma @@ -196,14 +196,14 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ + $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= - INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ + INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) @@ -314,7 +314,6 @@ NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) -DPVO:=$(call cat_vo_itarget, plugins/dp) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) XMLVO:= @@ -322,7 +321,7 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) @@ -347,8 +346,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 -DATE=$(shell LANG=C date +"%B %Y") - ########################################################################### # Source documentation ########################################################################### diff --git a/Makefile.doc b/Makefile.doc index 59eb2fe8..685887f5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -12,7 +12,7 @@ ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial -.PHONY: stdlib full-stdlib faq rectutorial +.PHONY: stdlib full-stdlib faq rectutorial refman-html-dir INDEXURLS:=doc/refman/html/index_urls.txt @@ -126,14 +126,16 @@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html ALLINDEXES:= doc/refman/html/index.html $(INDEXES) -$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ +$(ALLINDEXES): refman-html-dir + +refman-html-dir: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html - $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html + -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: (cd doc/refman;\ @@ -200,40 +202,32 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) ifdef QUICK -doc/stdlib/index-body.html: - - rm -rf doc/stdlib/html - $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ - -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html +doc/stdlib/html/genindex.html: else -doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) +doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) +endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ + $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ -R theories Coq $(THEORIESVO:.vo=.v) - mv doc/stdlib/html/index.html doc/stdlib/index-body.html -endif + mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index - ./doc/stdlib/make-library-index doc/stdlib/index-list.html + ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files -doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html - cat doc/stdlib/index-list.html > $@ - sed -n -e '//,/<\/table>/p' doc/stdlib/index-body.html >> $@ - cat doc/stdlib/index-trailer.html >> $@ +doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html + cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@ + cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@ ### Standard library (light version, full version is definitely too big) ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ else -doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ +doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ @@ -255,12 +249,12 @@ ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) > $@ - sed -i "" -e 's///g' $@ + sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) > $@ - sed -i "" -e 's///g' $@ + sed -i.tmp -e 's///g' $@ && rm $@.tmp endif doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex diff --git a/README b/README index 4f4afa5b..9bf63c43 100644 --- a/README +++ b/README @@ -38,7 +38,7 @@ THE COQ CLUB. discuss questions about the Coq system and related topics. The submission address is: - coq-club@coq.inria.fr + coq-club@inria.fr The topics to be discussed in the club should include: @@ -55,7 +55,7 @@ THE COQ CLUB. To be added to, or removed from, the mailing list, please write to: - coq-club-request@coq.inria.fr + coq-club-request@inria.fr Please use also this address for any questions/suggestions about the Coq Club. It might sometimes take a few days before your messages get @@ -67,7 +67,7 @@ BUGS REPORT. Send your bug reports by filling a form at - http://logical.saclay.inria.fr/coq-bugs + http://coq.inria.fr/bugs To be effective, bug reports should mention the Caml version used to compile and run Coq, the Coq version (coqtop -v), the configuration diff --git a/TODO b/TODO deleted file mode 100644 index d6891e5f..00000000 --- a/TODO +++ /dev/null @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme ) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9942816d..e3431fec 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -53,10 +53,14 @@ let path_of_mexpr = function | SEBident mp -> mp | _ -> raise Not_path -let rec list_split_assoc k rev_before = function +let is_modular = function + | SFBmodule _ | SFBmodtype _ -> true + | SFBconst _ | SFBmind _ -> false + +let rec list_split_assoc ((k,m) as km) rev_before = function | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail + | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after + | h::tail -> list_split_assoc km (h::rev_before) tail let check_definition_sub env cb1 cb2 = let check_type env t1 t2 = @@ -131,38 +135,35 @@ let lookup_modtype mp env = let rec check_with env mtb with_decl mp= match with_decl with - | With_definition_body _ -> - check_with_aux_def env mtb with_decl mp; + | With_definition_body (idl,c) -> + check_with_def env mtb (idl,c) mp; mtb - | With_module_body _ -> - check_with_aux_mod env mtb with_decl mp; + | With_module_body (idl,mp1) -> + check_with_mod env mtb (idl,mp1) mp; mtb -and check_with_aux_def env mtb with_decl mp = +and check_with_def env mtb (idl,c) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_definition_body ([],_) -> assert false - | With_definition_body ([id],c) -> + if idl = [] then let cb = match spec with SFBconst cb -> cb | _ -> error_not_a_constant l in check_definition_sub env' c cb - | With_definition_body (_::_,_) -> + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -170,49 +171,36 @@ and check_with_aux_def env mtb with_decl mp = begin match old.mod_expr with | None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l)) + check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl mp = +and check_with_mod env mtb (idl,mp1) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in let before = List.rev rev_before in - let rec mp_rec = function - | [] -> mp - | i::r -> MPdot(mp_rec r,label_of_id i) - in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_module_body ([],_) -> assert false - | With_module_body ([id], mp1) -> + if idl = [] then let _ = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l in let (_:module_body) = (lookup_module mp1 env) in () - | With_module_body (_::_,mp) -> + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -220,17 +208,11 @@ and check_with_aux_mod env mtb with_decl mp = begin match old.mod_expr with None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_mod env' - old.mod_type new_with_decl (MPdot(mp,l)) + check_with_mod env' + old.mod_type (idl,mp1) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0c97254b..9870ba13 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -28,15 +28,18 @@ type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body + +type namedmodule = | Module of module_body | Modtype of module_type_body (* adds above information about one mutual inductive: all types and constructors *) -let add_nameobjects_of_mib ln mib map = - let add_nameobjects_of_one j oib map = - let ip = (ln,j) in +let add_mib_nameobjects mp l mib map = + let ind = make_mind mp empty_dirpath l in + let add_mip_nameobjects j oib map = + let ip = (ind,j) in let map = array_fold_right_i (fun i id map -> @@ -46,22 +49,32 @@ let add_nameobjects_of_mib ln mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_nameobjects_of_one mib.mind_packets map + array_fold_right_i add_mip_nameobjects mib.mind_packets map + + +(* creates (namedobject/namedmodule) map for the whole signature *) +type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } -(* creates namedobject map for the whole signature *) +let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } -let make_label_map mp list = +let get_obj mp map l = + try Labmap.find l map.objs + with Not_found -> error_no_such_label_sub l mp + +let get_mod mp map l = + try Labmap.find l map.mods + with Not_found -> error_no_such_label_sub l mp + +let make_labmap mp list = let add_one (l,e) map = - let add_map obj = Labmap.add l obj map in match e with - | SFBconst cb -> add_map (Constant cb) - | SFBmind mib -> - add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map - | SFBmodule mb -> add_map (Module mb) - | SFBmodtype mtb -> add_map (Modtype mtb) + | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } + | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } in - List.fold_right add_one list Labmap.empty + List.fold_right add_one list empty_labmap let check_conv_error error f env a1 a2 = @@ -282,7 +295,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 - | _ -> error () let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in @@ -291,29 +303,25 @@ let rec check_modules env msb1 msb2 subst1 subst2 = and check_signatures env mp1 sig1 sig2 subst1 subst2 = - let map1 = make_label_map mp1 sig1 in + let map1 = make_labmap mp1 sig1 in let check_one_body (l,spec2) = - let info1 = - try - Labmap.find l map1 - with - Not_found -> error_no_such_label_sub l mp1 - in match spec2 with | SFBconst cb2 -> - check_constant env mp1 l info1 cb2 spec2 subst1 subst2 + check_constant env mp1 l (get_obj mp1 map1 l) + cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive env mp1 l info1 mib2 spec2 subst1 subst2 + check_inductive env mp1 l (get_obj mp1 map1 l) + mib2 spec2 subst1 subst2 | SFBmodule msb2 -> begin - match info1 with + match get_mod mp1 map1 l with | Module msb -> check_modules env msb msb2 subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> let mtb1 = - match info1 with + match get_mod mp1 map1 l with | Modtype mtb -> mtb | _ -> error_not_match l spec2 in diff --git a/configure b/configure index 867ee935..44170b99 100755 --- a/configure +++ b/configure @@ -6,10 +6,10 @@ # ################################## -VERSION=8.4beta +VERSION=8.4beta2 VOMAGIC=08400 STATEMAGIC=58400 -DATE="December 2011" +DATE=`LC_ALL=C LANG=C date +"%B %Y"` # Create the bin/ directory if non-existent test -d bin || mkdir bin @@ -292,7 +292,7 @@ case $DATEPGM in "") echo "I can't find the program \"date\" in your path." echo "Please give me the current date" read COMPILEDATE;; - *) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;; + *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;; esac # Architecture @@ -388,7 +388,7 @@ fi if [ "$browser_spec" = "no" ]; then case $ARCH in - win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;; + win32) BROWSER='start %s' ;; Darwin) BROWSER='open %s' ;; *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;; esac @@ -445,16 +445,16 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.0*) + 1.*|2.*|3.0*|3.10*|3.11.[01]) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.10.0 or later." + echo " You need Objective-Caml 3.11.2 or later." echo " Configuration script failed!" exit 1 fi;; - 3.1*) + 3.11.2|3.12*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) @@ -742,7 +742,7 @@ case $ARCH$CYGWIN in bindir_def=${W32PREF}bin libdir_def=${W32PREF}lib configdir_def=${W32PREF}config - datadir_def=${W32PREF}data + datadir_def=${W32PREF}share mandir_def=${W32PREF}man docdir_def=${W32PREF}doc emacslib_def=${W32PREF}emacs @@ -795,10 +795,15 @@ case $libdir_spec in *) LIBDIR_OPTION="None";; esac -case $configdir_spec/$local in - yes/*) CONFIGDIR=$configdir;; - */true) CONFIGDIR=$COQTOP/ide - configdir_spec=yes;; +case $configdir_spec/$prefix_spec/$local in + yes/*/*) CONFIGDIR=$configdir;; + */yes/*) configdir_spec=yes + case $ARCH in + win32) CONFIGDIR=$prefix/config;; + *) CONFIGDIR=$prefix/etc/xdg/coq;; + esac;; + */*/true) CONFIGDIR=$COQTOP/ide + configdir_spec=yes;; *) printf "Where should I install the Coqide configuration files [$configdir_def]? " read CONFIGDIR case $CONFIGDIR in diff --git a/dev/base_include b/dev/base_include index d1125965..ad2a3aec 100644 --- a/dev/base_include +++ b/dev/base_include @@ -123,7 +123,6 @@ open Decl_mode open Auto open Autorewrite open Contradiction -open Dhyp open Eauto open Elim open Equality @@ -199,6 +198,11 @@ let current_goal () = get_nth_goal 1;; let pf_e gl s = Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; +(* Set usual printing since the global env is available from the tracer *) +let _ = Constrextern.in_debugger := false +let _ = Constrextern.set_debug_global_reference_printer + (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + open Toplevel let go = loop diff --git a/dev/printers.mllib b/dev/printers.mllib index 6a42678e..40a5a822 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -105,12 +105,12 @@ Notation Dumpglob Reserve Impargs -Constrextern Syntax_def Implicit_quantifiers Smartlocate Constrintern Modintern +Constrextern Tacexpr Proof_type Goal diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3fc90761..3116cbf2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -487,5 +487,9 @@ let short_string_of_ref loc = function [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)] (id_of_string ("_"^string_of_int j)) +(* Anticipate that printers can be used from ocamldebug and that + pretty-printer should not make calls to the global env since ocamldebug + runs in a different process and does not have the proper env at hand *) +let _ = Constrextern.in_debugger := true let _ = Constrextern.set_debug_global_reference_printer (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index f0fb0883..ce998a9b 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -206,6 +206,7 @@ %END LATEX %HEVEA \renewcommand{\proof}{\nterm{proof}} \newcommand{\record}{\nterm{record}} +\newcommand{\recordkw}{\nterm{record\_keyword}} \newcommand{\rewrule}{\nterm{rewriting\_rule}} \newcommand{\sentence}{\nterm{sentence}} \newcommand{\simplepattern}{\nterm{simple\_pattern}} diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index f4809a48..62ee00ac 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -27,7 +27,6 @@