diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:48 +0000 |
| commit | 30cf9c6711df3eb583dacad3cb98158adbbf1f5f (patch) | |
| tree | dbb893378505ee744b94b4d8ef051018dac9d813 /toplevel/lemmas.ml | |
| parent | 3ab6c3a21f569ec684737e45200aa1b32f009214 (diff) | |
remove useless hidden_flag in TacMutual(Co)Fix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/lemmas.ml')
| -rw-r--r-- | toplevel/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 1c8302c1a..747f5835f 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -260,7 +260,7 @@ let start_proof id kind c ?init_tac ?(compute_guard=[]) hook = let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun (id,(t,_)) -> (id,t)) thms with - | (id,_)::l -> Hiddentac.h_mutual_cofix true id l + | (id,_)::l -> Hiddentac.h_mutual_cofix id l | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) @@ -268,7 +268,7 @@ let rec_tac_initializer finite guard thms snl = | None -> List.map succ (List.map List.last guard) | Some nl -> nl in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l + | (id,n,_)::l -> Hiddentac.h_mutual_fix id n l | _ -> assert false let start_proof_with_initialization kind recguard thms snl hook = |