diff options
| author | filliatr | 2000-11-21 16:54:58 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-21 16:54:58 +0000 |
| commit | cb5af55e2500748daa62c11f92c53f72e37d49c4 (patch) | |
| tree | 0a60bf89e6d9f50b6631b079a40b3e6f882e4070 /toplevel | |
| parent | c332c8fe84f7a2f1abbde26a95a369934ed82487 (diff) | |
implicites manuels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 25 |
2 files changed, 18 insertions, 9 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index ba584d756e..866d09f7d3 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -173,7 +173,7 @@ let process_object oldenv dir sec_sp | "INDUCTIVE" -> let mib = Environ.lookup_mind sp oldenv in let newsp = recalc_sp dir sp in - let imp = is_implicit_inductive_definition sp in + let imp = is_implicit_args() (* CHANGE *) in let (mie,indmods,cstrmods) = process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in ((Inductive(mie,imp)) :: ops, ids_to_discard, diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f60ecbd3e4..e33c9655a3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -436,6 +436,21 @@ let _ = | [] -> (fun () -> Impargs.make_implicit_args false) | _ -> bad_vernac_args "IMPLICIT_ARGS_OFF") +let number_list = + List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list") + +let _ = + add "IMPLICITS" + (function + | (VARG_STRING "") :: (VARG_IDENTIFIER id) :: l -> + (fun () -> + let imps = number_list l in + Impargs.declare_manual_implicits (Nametab.sp_of_id CCI id) imps) + | [VARG_STRING "Auto"; VARG_IDENTIFIER id] -> + (fun () -> + Impargs.declare_implicits (Nametab.sp_of_id CCI id)) + | _ -> bad_vernac_args "IMPLICITS") + let _ = add "SaveNamed" (function @@ -588,10 +603,7 @@ let _ = let _ = add "ExplainProof" (function l -> - let l = List.map (function - | (VARG_NUMBER n) -> n - | _ -> bad_vernac_args "ExplainProof") l - in + let l = number_list l in fun () -> let pts = get_pftreestate() in let evc = evc_of_pftreestate pts in @@ -605,10 +617,7 @@ let _ = let _ = add "ExplainProofTree" (function l -> - let l = List.map (function - | (VARG_NUMBER n) -> n - | _ -> bad_vernac_args "ExplainProofTree") l - in + let l = number_list l in fun () -> let pts = get_pftreestate() in let evc = evc_of_pftreestate pts in |