diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:04 +0000 |
| commit | c8c8ad4811b5c4a8ee2e55a66d69e175d132da25 (patch) | |
| tree | add19673065a2696292a5254bd08286c1d3ce586 /pretyping/tacred.ml | |
| parent | dcc959231afc24a9e766445f90c031f94ba85282 (diff) | |
Slight cosmetic cleaning of tacred.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e99baa291..90e0683c0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -686,7 +686,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = with Redelimination -> match reference_opt_value sigma env ref with | Some c -> - (match kind_of_term ((strip_lam c)) with + (match kind_of_term (strip_lam c) with | CoFix _ | Fix _ -> s | _ -> redrec (c, stack)) | None -> s) @@ -696,7 +696,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = (* Same as [whd_simpl] but also reduces constants that do not hide a reducible fix, but does this reduction of constants only until it - it immediately hides a non reducible fix or a cofix *) + immediately hides a non reducible fix or a cofix *) let whd_simpl_orelse_delta_but_fix env sigma c = let rec redrec s = @@ -704,7 +704,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = if isEvalRef env constr then match reference_opt_value sigma env (destEvalRef constr) with | Some c -> - (match kind_of_term ((strip_lam c)) with + (match kind_of_term (strip_lam c) with | CoFix _ | Fix _ -> s' | _ -> redrec (c, stack)) | None -> s' |